Nuprl Definition : testxx
testxx(x;y)==r if (x =z 0) then y else testxx(x - 1;y) fi
testxx(x;y) == fix((λtestxx,x. if (x =z 0) then y else testxx (x - 1) fi )) x
Definitions occuring in Statement :
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
apply: f a,
fix: fix(F),
lambda: λx.A[x],
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
fix: fix(F),
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 :
testxx
Latex:
testxx(x;y)==r if (x =\msubz{} 0) then y else testxx(x - 1;y) fi
Latex:
testxx(x;y) == fix((\mlambda{}testxx,x. if (x =\msubz{} 0) then y else testxx (x - 1) fi )) x
Date html generated:
2016_05_14-PM-09_33_05
Last ObjectModification:
2015_09_22-PM-06_03_26
Theory : num_thy_1
Home
Index