Zulip Chat Archive

Stream: general

Topic: failed to add declaration

Keeley Hoek (Sep 15 2018 at 12:58):

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

Keeley Hoek (Sep 15 2018 at 12:59):

How can I see what the metavariables are?

Simon Hudon (Sep 15 2018 at 19:43):

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

Last updated: Dec 20 2023 at 11:08 UTC