Nuprl Definition : isqrt2
isqrt2(x) ==
letrec sqrt(i)=if i=0 then 0 else eval r = (sqrt (i ÷ 4)) * 2 in if (r * (r + 2)) < (i) then r + 1 else r in
sqrt
x
Definitions occuring in Statement :
natrec: natrec,
callbyvalue: callbyvalue,
less: if (a) < (b) then c else d,
int_eq: if a=b then c else d,
apply: f a,
divide: n ÷ m,
multiply: n * m,
add: n + m,
natural_number: $n
Definitions occuring in definition :
natrec: natrec,
int_eq: if a=b then c else d,
callbyvalue: callbyvalue,
apply: f a,
divide: n ÷ m,
less: if (a) < (b) then c else d,
multiply: n * m,
add: n + m,
natural_number: $n
FDL editor aliases :
isqrt2
Latex:
isqrt2(x) ==
letrec sqrt(i)=if i=0
then 0
else eval r = (sqrt (i \mdiv{} 4)) * 2 in
if (r * (r + 2)) < (i) then r + 1 else r in
sqrt
x
Date html generated:
2016_05_15-PM-11_39_41
Last ObjectModification:
2015_09_23-AM-08_30_55
Theory : rationals
Home
Index