Nuprl Definition : colength

colength(L)==r if L = Ax then 0 otherwise let a,b = L in 1 + colength(b)

colength(L) == fix((λcolength,L. if L = Ax then 0 otherwise let a,b = L in 1 + (colength b))) L

Definitions occuring in Statement : isaxiom: if z = Ax then a otherwise b, apply: f a, fix: fix(F), lambda: λx.A[x], spread: spread def, add: n + m, natural_number: $n
Definitions occuring in definition : fix: fix(F), lambda: λx.A[x], isaxiom: if z = Ax then a otherwise b, spread: spread def, add: n + m, natural_number: $n, apply: f a
FDL editor aliases : colength

Latex:
colength(L)==r if L = Ax then 0 otherwise let a,b = L in 1 + colength(b)

Latex:
colength(L) == fix((\mlambda{}colength,L. if L = Ax then 0 otherwise let a,b = L in 1 + (colength b))) L Date html generated: 2016_05_14-AM-06_25_28 Last ObjectModification: 2015_12_03-PM-02_04_41 Theory : list_0 Home Index