English
For integers m and n, Int.range(m,n) lists precisely the integers r with m ≤ r < n; equivalently, Int.range(m,n) = [m, m+1, ..., n-1] (empty if n ≤ m).
Русский
Для целых m и n функция Int.range(m,n) точно перечисляет целые r такие, что m ≤ r < n; эквивалентно Int.range(m,n) = [m, m+1, ..., n-1] (пустой список при n ≤ m).
LaTeX
$$$\text{Int.range}(m,n) = [m, m+1, \dots, n-1] \quad (\text{пусть } n>m; \text{ иначе пусто})$$$
Lean4
/-- List enumerating `[m, n)`. This is the ℤ variant of `List.Ico`. -/
def range (m n : ℤ) : List ℤ :=
((List.range (toNat (n - m))) : List ℕ).map fun (r : ℕ) => (m + r : ℤ)
