custom recursor

Stream: general

[Simon Hudon]

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]

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

[Mario Carneiro]

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]

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]

Maybe I should just add that to my wish list