Zulip Chat Archive

If I define an inductive type, then its rec_on gives a different type which can be quite complex. I have some intuition on how it this works, but is it maybe explicitly written down somewhere?
Thanks.

Kevin Buzzard (Oct 17 2020 at 22:01):

presumably this is in Mario's MSc thesis?

Marc Huisinga (Oct 17 2020 at 22:20):

there's also a natural language description here: https://leanprover.github.io/reference/declarations.html#inductive-families

Golol (Oct 17 2020 at 22:43):

perfect, that's exactly what I was looking for

Chris B (Oct 17 2020 at 22:51):

@Golol
Also you may have noticed, but rec_on is just a definition that rearranges the order of the arguments passed to rec. rec_on takes the major as the first explicit argument since it's often more intuitive (it feels more like telling the computer "do induction on n").
If you're going to read Mario's thesis you might like having the mm0 spec as a guide even if you don't speak mm0 (https://github.com/digama0/mm0/blob/master/examples/lean.mm1#L284).
There are four type checkers to choose from if you want to see actually see source code that constructs a recursor, but it's fairly involved. It's still pretty neat though.