Nuprl Definition : cons-seq
cons-seq(x;s) == λn.if (n =z 0) then x else s (n - 1) fi
Definitions occuring in Statement :
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
apply: f a,
lambda: λx.A[x],
subtract: n - m,
natural_number: $n
Definitions :
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
apply: f a,
subtract: n - m,
natural_number: $n
FDL editor aliases :
cons-seq
cons-seq(x;s) == \mlambda{}n.if (n =\msubz{} 0) then x else s (n - 1) fi
Date html generated:
2015_07_17-AM-07_58_33
Last ObjectModification:
2008_02_27-PM-05_47_43
Home
Index