Nuprl Definition : listify
listify(f;m;n) == fix((λlistify,m. if n ≤z m then [] else [f m / (listify (m + 1))] fi )) m
Definitions occuring in Statement :
cons: [a / b],
nil: [],
le_int: i ≤z j,
ifthenelse: if b then t else f fi ,
apply: f a,
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 ,
le_int: i ≤z j,
nil: [],
cons: [a / b],
apply: f a,
add: n + m,
natural_number: $n
FDL editor aliases :
listify
Latex:
listify(f;m;n) == fix((\mlambda{}listify,m. if n \mleq{}z m then [] else [f m / (listify (m + 1))] fi )) m
Date html generated:
2016_05_14-AM-06_26_10
Last ObjectModification:
2015_12_03-PM-02_06_21
Theory : list_0
Home
Index