Zulip Chat Archive

Stream: new members

Topic: How to get rec_on from an inductive type?

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. 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.

Morten Brodersen (Jul 18 2021 at 10:31):

I have searched for "Mario's MSc thesis" without results. Can somebody point me in the right direction? Thanks!

Morten Brodersen (Jul 18 2021 at 10:35):

OK found out that Mario is Mario Carneiro. Found it!

Mario Carneiro (Jul 18 2021 at 10:57):

the relevant link is https://github.com/digama0/lean-type-theory/releases/tag/v1.0

Morten Brodersen (Jul 18 2021 at 10:58):

Yep found it Mario. I will give it a read.

Last updated: Dec 20 2023 at 11:08 UTC