Integer division

The integer division or quotient of two numbers, written //, is the result of the division rounded down to the nearest integer. Intuitively, you can think of it as the number of times that one thing fits into another, disregarding any remainder. For example, 11 // 2 is 5, because 2 fits into 11 five times (with some left over).

Disco> 11 // 2
5
Disco> 6 // 2
3
Disco> 6 // 7
0
Disco> (-7) // 2
-4

In fact, // is simply defined in terms of regular division as well as the floor operation:

x // y = floor (x / y)

Although dividing two integers using the usual / operator does not necessarily result in an integer, using integer division does. In particular, the integer division operator can be given the types

~//~ : ℕ × ℕ → ℕ
~//~ : ℤ × ℤ → ℤ

Formally, the result of // is defined in terms of the “Division Algorithm”: given a number \(n\) and a divisor \(d\), the quotient n // d is the unique number \(q\) such that \(n = qd + r\), where \(0 \leq r < d\).