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.
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.
It is possible to obtain both the quotient and remainder together, by means of the predefined function
ediv
: See optional values.