Skip to main content

Numerical operators

+

(+ x y)
(+ x y)
  • takes x: a
  • takes y: a
  • produces a
  • where a is of type integer or decimal

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 integer or decimal

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 integer or decimal

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 integer or decimal

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 integer or decimal

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 integer or decimal

Logarithm of x base b.

Supported in either invariants or properties.

-

(- x)
(- x)
  • takes x: a
  • produces a
  • where a is of type integer or decimal

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 integer or decimal

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 integer or decimal

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 integer or decimal

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 integer or decimal

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.

Bitwise


Receive important developer updates