Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC