rec_name

Stream: general

[Jakob von Raumer]

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?

[Sebastian Ullrich]

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

[Sebastian Ullrich]

Good to know that induction works at all

[Jakob von Raumer]

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

[Sebastian Ullrich]

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

[Sebastian Ullrich]

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

[Jakob von Raumer]

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...