Nuprl Definition : halfpi
π/2 == λn.eval m = 4 * n in eval m2 = 2 * m in eval N = cubic_converge(100000000000000000000;m2) in fastpi(N) m ÷ 4
Definitions occuring in Statement :
cubic_converge: cubic_converge(b;m),
fastpi: fastpi(n),
callbyvalue: callbyvalue,
apply: f a,
lambda: λx.A[x],
divide: n ÷ m,
multiply: n * m,
natural_number: $n
Definitions occuring in definition :
natural_number: $n,
fastpi: fastpi(n),
apply: f a,
cubic_converge: cubic_converge(b;m),
callbyvalue: callbyvalue,
multiply: n * m,
divide: n ÷ m,
lambda: λx.A[x]
FDL editor aliases :
halfpi
Latex:
\mpi{}/2 ==
\mlambda{}n.eval m = 4 * n in
eval m2 = 2 * m in
eval N = cubic\_converge(100000000000000000000;m2) in
fastpi(N) m \mdiv{} 4
Date html generated:
2016_10_26-PM-00_22_50
Last ObjectModification:
2016_09_12-PM-05_42_34
Theory : reals_2
Home
Index