Nuprl Definition : genfact
genfact(n;b;m.f[m]) ==
if (n) < (1) then b else eval x = f[n] in eval b' = b * x in eval n' = n - 1 in genfact(n';b';m.f[m])
Definitions occuring in Statement :
callbyvalue: callbyvalue,
less: if (a) < (b) then c else d,
multiply: n * m,
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
less: if (a) < (b) then c else d,
multiply: n * m,
callbyvalue: callbyvalue,
subtract: n - m,
natural_number: $n
FDL editor aliases :
genfact
Latex:
genfact(n;b;m.f[m]) ==
if (n) < (1)
then b
else eval x = f[n] in
eval b' = b * x in
eval n' = n - 1 in
genfact(n';b';m.f[m])
Date html generated:
2019_06_20-PM-02_25_31
Last ObjectModification:
2019_02_08-AM-11_02_15
Theory : num_thy_1
Home
Index