Zulip Chat Archive

Stream: new members

Topic: Examples of inductive family type constructors in Lean

view this post on Zulip Rajiv (Dec 09 2020 at 07:21):

I am trying to develop an intuition of how inductive families type constructors work in lean. I was wondering where I can find more examples of inductive type families in Lean standard library? So far, I've discovered eq and heq.

view this post on Zulip Marc Huisinga (Dec 09 2020 at 09:16):

the most important ones are probably eq and acc (well founded recursion).
there's an introduction to well founded recursion in lean here and you can find the definition here. a dependently-typed
vector is also often used as an example (although rarely used in practice), and inductive predicates come up a lot in general.

view this post on Zulip Rajiv (Dec 09 2020 at 11:27):

Thanks Marc for the pointers. I'll check it out.

Last updated: May 08 2021 at 10:12 UTC