Stream: new members
Golol (Oct 17 2020 at 21:59):
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?
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):
Also you may have noticed, but
rec_on is just a definition that rearranges the order of the arguments passed to
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.
Last updated: May 14 2021 at 02:15 UTC