failed to add declaration

Stream: general

[Keeley Hoek]

Has anyone ever seen the error failed to add declaration 'xxxx.my_defn' to environment, type has metavariables while writing a tactic?

[Keeley Hoek]

How can I see what the metavariables are?

[Simon Hudon]

mathlib has list_meta_vars in tactic.basic. It may be enough to just instantiate_mvars before adding your definition.