Zulip Chat Archive

Stream: new members

Topic: induction unknown declaration

Joachim Breitner (Feb 21 2022 at 15:08):

I am (again) trying to use my own induction rules. Oddly,

  induction w using neword.cons_induction,

simply says

unknown declaration 'neword.cons_induction'

although that is certainly a known declaration; tactics like refine find it just fine.

Any quick ideas? (I’ll just use refine manually for now)

Alex J. Best (Feb 21 2022 at 16:02):

Do you have a #mwe?

Yakov Pechersky (Feb 21 2022 at 16:07):

"using" needs a fully qualified name. So it's probably something like "free_group.neword.cons_induction"

Last updated: Dec 20 2023 at 11:08 UTC