## Stream: general

### Topic: custom recursor

#### Simon Hudon (Mar 02 2018 at 20:10):

I'm creating a recursor for a type that I defined and I'd like match and cases to pick it instead of what Lean generated. Is there a way to do that?

#### Andrew Ashworth (Mar 02 2018 at 20:20):

instead of cases, why not use inductionwhere you can specify the recursor?

#### Mario Carneiro (Mar 02 2018 at 20:23):

No, that's not really possible. You can use the usingclause of induction, but it's not particularly reliable in my experience. I don't really consider it supported

#### Simon Hudon (Mar 02 2018 at 20:28):

For cases on coinductive types, I can make my own tactics but it would be great if the same tactic could cover both inductive and coinductive types

#### Simon Hudon (Mar 02 2018 at 20:28):

Maybe I should just add that to my wish list

Last updated: May 11 2021 at 00:31 UTC