Nuprl Definition : colist
The co-recursive type of
all terms built from Ax (= []) and pairs <t, l> (= ⌜[t / l]⌝)
where ⌜t ∈ T⌝ and ⌜l ∈ colist(T)⌝. It includes both the finite lists and
infinite streams.⋅
colist(T) == corec(L.Unit ⋃ (T × L))
Definitions occuring in Statement :
corec: corec(T.F[T]),
b-union: A ⋃ B,
unit: Unit,
product: x:A × B[x]
Definitions occuring in definition :
corec: corec(T.F[T]),
b-union: A ⋃ B,
unit: Unit,
product: x:A × B[x]
FDL editor aliases :
colist
Latex:
colist(T) == corec(L.Unit \mcup{} (T \mtimes{} L))
Date html generated:
2016_07_08-PM-04_47_55
Last ObjectModification:
2015_12_03-PM-02_04_40
Theory : list_0
Home
Index