Zulip Chat Archive

Stream: general

Topic: rec_name


view this post on Zulip Jakob von Raumer (Mar 19 2018 at 13:34):

After adding an inductive type to the environment using add_inductive, I can use the induction tactic, but it doesn't return any useful case names... Can I solve this by defining rec_name?

view this post on Zulip Sebastian Ullrich (Mar 19 2018 at 13:38):

Sounds like it: https://github.com/leanprover/lean/blob/master/library/init/meta/tactic.lean#L425-L426

view this post on Zulip Sebastian Ullrich (Mar 19 2018 at 13:38):

Good to know that induction works at all

view this post on Zulip Jakob von Raumer (Mar 19 2018 at 13:52):

Yes, that's indeed a good thing. I don't even have to add the using clause...

view this post on Zulip Sebastian Ullrich (Mar 19 2018 at 13:53):

Apparently you do, if you want nice case names :)

view this post on Zulip Sebastian Ullrich (Mar 19 2018 at 13:54):

The alternative is to set the case names on your own, using a wrapper around the induction tactic

view this post on Zulip Jakob von Raumer (Mar 19 2018 at 13:58):

I don't _really_ need the case names so far, but I'm kind of feeling that I don't have enough control over which case belongs to which constructor while the tactic is working on it...


Last updated: May 11 2021 at 14:11 UTC