Skip to main content
Version: 1.4.0

Dividing

Because LIGO features neither floating-point nor fixed-point arithmetic, division in LIGO is Euclidean. The predefined binary operator / returns the quotient and is overloaded like the multiplication. Of course, division by zero triggers an exception that interrups the execution, so the programmer must make sure this case cannot happen because the compiler cannot determine, in general, if a variable will have a given value (or not) for all inputs.

const a : int = 10 / 3; // int / int yields int
const b : nat = 10n / 3n; // nat / nat yields nat
const c : int = 10n / 3; // nat / int yields int
const d : int = 10 / 3n; // int / nat yields int

The binary operator % returns the positive modulo of the Euclidean division, that is, the following holds:

(n*(a/n)+(a%n) == a) && (0n <= a % n) && (a % n < abs(n))

It is overloaded as the Euclidean division / to allow for all four combinations of natural numbers and integers.

const a : nat = 120 % 9; // int % int yields nat
const b : nat = 120n % 9; // nat % int yields nat
const c : nat = 120n % 9n; // nat % nat yields nat
const d : nat = 120 % 9n; // int % nat yields nat

It is possible to obtain both the quotient and remainder together, by means of the predefined function ediv: See optional values.