Examples of inductive family type constructors in Lean

Stream: new members

[Rajiv]

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]

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]

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