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):
tactic.basic. It may be enough to just
instantiate_mvars before adding your definition.
Last updated: Aug 03 2023 at 10:10 UTC