Nuprl Definition : int-rmul
k1 * a == eval k = k1 in λn.if (k) < (0) then -(a ((-k) * n)) else if (0) < (k) then a (k * n) else 0
Definitions occuring in Statement :
callbyvalue: callbyvalue,
less: if (a) < (b) then c else d,
apply: f a,
lambda: λx.A[x],
multiply: n * m,
minus: -n,
natural_number: $n
Definitions occuring in definition :
callbyvalue: callbyvalue,
lambda: λx.A[x],
minus: -n,
less: if (a) < (b) then c else d,
apply: f a,
multiply: n * m,
natural_number: $n
FDL editor aliases :
int-rmul
Latex:
k1 * a ==
eval k = k1 in
\mlambda{}n.if (k) < (0) then -(a ((-k) * n)) else if (0) < (k) then a (k * n) else 0
Date html generated:
2016_05_18-AM-06_55_16
Last ObjectModification:
2015_09_23-AM-09_00_53
Theory : reals
Home
Index