Nuprl Definition : polyconst
polyconst(n;k)==r if n=0 then k else if k=0 then [] else eval m = n - 1 in eval c = polyconst(m;k) in [c]
polyconst(n;k) ==
fix((λpolyconst,n. if n=0 then k else if k=0 then [] else eval m = n - 1 in eval c = polyconst m in [c])) n
Definitions occuring in Statement :
cons: [a / b],
nil: [],
callbyvalue: callbyvalue,
int_eq: if a=b then c else d,
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],
int_eq: if a=b then c else d,
subtract: n - m,
natural_number: $n,
callbyvalue: callbyvalue,
apply: f a,
cons: [a / b],
nil: []
FDL editor aliases :
polyconst
Latex:
polyconst(n;k)
==r if n=0 then k else if k=0 then [] else eval m = n - 1 in eval c = polyconst(m;k) in [c]
Latex:
polyconst(n;k) ==
fix((\mlambda{}polyconst,n. if n=0
then k
else if k=0 then [] else eval m = n - 1 in eval c = polyconst m in [c]))\000C
n
Date html generated:
2017_09_29-PM-06_00_21
Last ObjectModification:
2017_04_26-PM-02_04_54
Theory : integer!polynomials
Home
Index