Nuprl Definition : nat-to-str
nat-to-str(n) ==
fix((λnat-to-str,n. if (n =z 0) then [0]
if (n =z 1) then [1]
if (n =z 2) then [2]
if (n =z 3) then [3]
if (n =z 4) then [4]
if (n =z 5) then [5]
if (n =z 6) then [6]
if (n =z 7) then [7]
if (n =z 8) then [8]
if (n =z 9) then [9]
else (nat-to-str (n ÷ 10)) @ (nat-to-str (n rem 10))
fi ))
n
Definitions occuring in Statement :
append: as @ bs,
cons: [a / b],
nil: [],
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
apply: f a,
fix: fix(F),
lambda: λx.A[x],
remainder: n rem m,
divide: n ÷ m,
natural_number: $n,
token: "$token"
Definitions occuring in definition :
fix: fix(F),
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
cons: [a / b],
token: "$token",
nil: [],
append: as @ bs,
divide: n ÷ m,
apply: f a,
remainder: n rem m,
natural_number: $n
FDL editor aliases :
nat-to-str
Latex:
nat-to-str(n) ==
fix((\mlambda{}nat-to-str,n. if (n =\msubz{} 0) then [0]
if (n =\msubz{} 1) then [1]
if (n =\msubz{} 2) then [2]
if (n =\msubz{} 3) then [3]
if (n =\msubz{} 4) then [4]
if (n =\msubz{} 5) then [5]
if (n =\msubz{} 6) then [6]
if (n =\msubz{} 7) then [7]
if (n =\msubz{} 8) then [8]
if (n =\msubz{} 9) then [9]
else (nat-to-str (n \mdiv{} 10)) @ (nat-to-str (n rem 10))
fi ))
n
Date html generated:
2016_05_14-PM-03_35_10
Last ObjectModification:
2015_09_22-PM-06_01_09
Theory : decidable!equality
Home
Index