English
Ico n m is the list of natural numbers x with n ≤ x < m.
Русский
Ico n m — это список натуральных чисел x, удовлетворяющих n ≤ x < m.
LaTeX
$$$\operatorname{Ico}(n,m) = \operatorname{range}'(n,\,m-n)$$$
Lean4
/-- `Ico n m` is the list of natural numbers `n ≤ x < m`.
(Ico stands for "interval, closed-open".)
See also `Mathlib/Order/Interval/Basic.lean` for modelling intervals in general preorders, as well
as sibling definitions alongside it such as `Set.Ico`, `Multiset.Ico` and `Finset.Ico`
for sets, multisets and finite sets respectively.
-/
def Ico (n m : ℕ) : List ℕ :=
range' n (m - n)
