Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
a bare list of references, to be !include
-ed into the References-lists of relevant entries (inductive type, inductive familiy, inductive-recursive family, calculus of inductive constructions)
this list includes a polished-up version of
all the references previously listed at inductive familiy in the section “History” (due to revisions $\leq 5$ by Bas Spitters)
further references previously listed at inductive-recursive type
and some more
added pointer to:
and pointer to:
added earlier reference for the introduction of the notion of W-types:
following a hint in another thread (here)
1 to 4 of 4