Numerical operators
+
(+ x y)(+ x y)- takes
x: a - takes
y: a - produces a
- where a is of type
integerordecimal
Addition of integers and decimals.
Supported in either invariants or properties.
-
(- x y)(- x y)- takes
x: a - takes
y: a - produces a
- where a is of type
integerordecimal
Subtraction of integers and decimals.
Supported in either invariants or properties.
*
(* x y)(* x y)- takes
x: a - takes
y: a - produces a
- where a is of type
integerordecimal
Multiplication of integers and decimals.
Supported in either invariants or properties.
/
(/ x y)(/ x y)- takes
x: a - takes
y: a - produces a
- where a is of type
integerordecimal
Division of integers and decimals.
Supported in either invariants or properties.
^
(^ x y)(^ x y)- takes
x: a - takes
y: a - produces a
- where a is of type
integerordecimal
Exponentiation of integers and decimals.
Supported in either invariants or properties.
log
(log b x)(log b x)- takes
b: a - takes
x: a - produces a
- where a is of type
integerordecimal
Logarithm of x base b.
Supported in either invariants or properties.
-
(- x)(- x)- takes
x: a - produces a
- where a is of type
integerordecimal
Negation of integers and decimals.
Supported in either invariants or properties.
sqrt
(sqrt x)(sqrt x)- takes
x: a - produces a
- where a is of type
integerordecimal
Square root of integers and decimals.
Supported in either invariants or properties.
ln
(ln x)(ln x)- takes
x: a - produces a
- where a is of type
integerordecimal
Logarithm of integers and decimals base e.
Supported in either invariants or properties.
exp
(exp x)(exp x)- takes
x: a - produces a
- where a is of type
integerordecimal
Exponential of integers and decimals. e raised to the integer or decimal x.
Supported in either invariants or properties.
abs
(abs x)(abs x)- takes
x: a - produces a
- where a is of type
integerordecimal
Absolute value of integers and decimals.
Supported in either invariants or properties.
round
(round x)(round x)- takes
x:decimal - produces
integer
(round x prec)(round x prec)- takes
x:decimal - takes
prec:integer - produces
integer
Banker's rounding value of decimal x as integer, or to prec precision as
decimal.
Supported in either invariants or properties.
ceiling
(ceiling x)(ceiling x)- takes
x:decimal - produces
integer
(ceiling x prec)(ceiling x prec)- takes
x:decimal - takes
prec:integer - produces
integer
Rounds the decimal x up to the next integer, or to prec precision as
decimal.
Supported in either invariants or properties.
floor
(floor x)(floor x)- takes
x:decimal - produces
integer
(floor x prec)(floor x prec)- takes
x:decimal - takes
prec:integer - produces
integer
Rounds the decimal x down to the previous integer, or to prec precision as
decimal.
Supported in either invariants or properties.
dec
(dec x)(dec x)- takes
x:integer - produces
decimal
Casts the integer x to its decimal equivalent.
Supported in either invariants or properties.
mod
(mod x y)(mod x y)- takes
x:integer - takes
y:integer - produces
integer
Integer modulus
Supported in either invariants or properties.