## Stream: new members

### Topic: Examples of inductive family type constructors in Lean

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

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

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