Nuprl Definition : minus-polynom
minus-polynom(n;p)==r if n=0 then -p else map(λq.minus-polynom(n - 1;q);p)
minus-polynom(n;p) == fix((λminus-polynom,n,p. if n=0 then -p else map(λq.(minus-polynom (n - 1) q);p))) n p
Definitions occuring in Statement :
map: map(f;as)
,
int_eq: if a=b then c else d
,
apply: f a
,
fix: fix(F)
,
lambda: λx.A[x]
,
subtract: n - m
,
minus: -n
,
natural_number: $n
Definitions occuring in definition :
natural_number: $n
,
subtract: n - m
,
apply: f a
,
lambda: λx.A[x]
,
map: map(f;as)
,
minus: -n
,
int_eq: if a=b then c else d
,
fix: fix(F)
FDL editor aliases :
minus-polynom
Latex:
minus-polynom(n;p)==r if n=0 then -p else map(\mlambda{}q.minus-polynom(n - 1;q);p)
Latex:
minus-polynom(n;p) ==
fix((\mlambda{}minus-polynom,n,p. if n=0 then -p else map(\mlambda{}q.(minus-polynom (n - 1) q);p))) n p
Date html generated:
2017_04_20-AM-07_11_06
Last ObjectModification:
2017_04_19-AM-10_21_08
Theory : list_1
Home
Index