Nuprl Definition : list
The list type was once a primitive in Nuprl. Later, it was defined using
the "Mendler" fixpoint type. Now we define lists as those "co-lists"
for which the length (a partially defined function) has a value.
Once we show that the list iterator is well formed (see list_ind_wf)
then we can use list as an abstract type. This "implementation" shows that
we only need induction on ⌜ℕ⌝ to build lists, and do not need the power
of the Mendler fixpoint or a general inductive construction.⋅
T List == {L:colist(T)| (colength(L))↓}
Definitions occuring in Statement :
colength: colength(L),
colist: colist(T),
has-value: (a)↓,
set: {x:A| B[x]}
Definitions occuring in definition :
set: {x:A| B[x]} ,
colist: colist(T),
has-value: (a)↓,
colength: colength(L)
Rules referencing :
barInduction
Latex:
T List == \{L:colist(T)| (colength(L))\mdownarrow{}\}
Date html generated:
2016_07_08-PM-04_47_57
Last ObjectModification:
2015_12_03-PM-02_04_41
Theory : list_0
Home
Index