Nuprl Definition : ml-length
ml-length(l) == fix((λlength,l. if null(l) then 0 else let a.as = l in 1 + length(as) fi ))(l)
Definitions occuring in Statement :
spreadcons: spreadcons,
ml_apply: f(x)
,
null: null(as)
,
ifthenelse: if b then t else f fi
,
fix: fix(F)
,
lambda: λx.A[x]
,
add: n + m
,
natural_number: $n
Definitions occuring in definition :
fix: fix(F)
,
lambda: λx.A[x]
,
ifthenelse: if b then t else f fi
,
null: null(as)
,
spreadcons: spreadcons,
add: n + m
,
natural_number: $n
,
ml_apply: f(x)
FDL editor aliases :
ml-length
Latex:
ml-length(l) == fix((\mlambda{}length,l. if null(l) then 0 else let a.as = l in 1 + length(as) fi ))(l)
Date html generated:
2017_09_29-PM-05_50_52
Last ObjectModification:
2017_05_10-PM-06_33_48
Theory : ML
Home
Index