## Stream: general

### Topic: rec_name

#### 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?

#### Sebastian Ullrich (Mar 19 2018 at 13:38):

Good to know that induction works at all

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

#### Sebastian Ullrich (Mar 19 2018 at 13:53):

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

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

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