Stream: new members
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
Marc Huisinga (Dec 09 2020 at 09:16):
the most important ones are probably
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