Zulip Chat Archive

Stream: general

Topic: custom recursor


view this post on Zulip 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?

view this post on Zulip Andrew Ashworth (Mar 02 2018 at 20:20):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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