Skip to content

Commit

Permalink
docs(data/int/range): add module docstring (#7971)
Browse files Browse the repository at this point in the history
  • Loading branch information
YaelDillies committed Jun 17, 2021
1 parent da1a32c commit 93d7812
Showing 1 changed file with 12 additions and 1 deletion.
13 changes: 12 additions & 1 deletion src/data/int/range.lean
Expand Up @@ -6,11 +6,22 @@ Authors: Mario Carneiro, Kenny Lau
import data.int.basic
import data.list.range

/-!
# Intervals in ℤ
This file defines integer ranges. `range m n` is the set of integers greater than `m` and strictly
less than `n`.
## Note
This could be unified with `data.list.intervals`. See the TODOs there.
-/

namespace int

local attribute [semireducible] int.nonneg

/-- List enumerating `[m, n)`. -/
/-- List enumerating `[m, n)`. This is the ℤ variant of `list.Ico`. -/
def range (m n : ℤ) : list ℤ :=
(list.range (to_nat (n-m))).map $ λ r, m+r

Expand Down

0 comments on commit 93d7812

Please sign in to comment.