Nuprl Definition : rless-case
rless-case(x;y;n;z) == eval m = (12 * n) + 1 in if ((x m) + 4) < (z m) then inl m else (inr m )
Definitions occuring in Statement :
callbyvalue: callbyvalue,
less: if (a) < (b) then c else d,
apply: f a,
inr: inr x ,
inl: inl x,
multiply: n * m,
add: n + m,
natural_number: $n
Definitions occuring in definition :
callbyvalue: callbyvalue,
multiply: n * m,
less: if (a) < (b) then c else d,
add: n + m,
natural_number: $n,
apply: f a,
inl: inl x,
inr: inr x
FDL editor aliases :
rless-case
Latex:
rless-case(x;y;n;z) == eval m = (12 * n) + 1 in if ((x m) + 4) < (z m) then inl m else (inr m )
Date html generated:
2016_05_18-AM-07_32_11
Last ObjectModification:
2015_09_23-AM-09_01_50
Theory : reals
Home
Index