# Zulip Chat Archive

## Stream: new members

### Topic: range

#### Kana (Feb 18 2021 at 15:26):

Is there somewhere in the stdlib `range`

function?

Right now I make it myself

```
class has_range (α : Type) := { range : α → α → list α }
infix `..`:50 := has_range.range
namespace nat
private def range' : ℕ → ℕ → list ℕ
| 0 0 := [0]
| a 0 := []
| a b@(b'+1) := if b >= a then b::range' a b' else []
protected def range (a b : ℕ) : list ℕ :=
(range' a b).reverse
instance : has_range ℕ := { range := nat.range }
end nat
namespace char
protected def range (a : char) (b : char ) : list char :=
char.of_nat <$> (a.to_nat .. b.to_nat)
instance : has_range char := { range := char.range }
end char
#eval 'a'..'z'
#eval 'A'..'z'
#eval 10..20
#eval 1..0
```

#### Eric Wieser (Feb 18 2021 at 15:30):

@Anne Baanen had a branch where they were working on this (edit: branch#fin_range)

#### Yakov Pechersky (Feb 18 2021 at 15:42):

In the meantime, you can use list.map of list.range or list.range'

#### Kana (Feb 18 2021 at 15:52):

Thanks. No I have

```
class has_range (α : Type) :=
(range : α → α → list α)
infix `..`:50 := has_range.range
instance : has_range ℕ :=
{ range := λ a b, (+ a) <$> list.range (b + 1 - a) }
instance : has_range char :=
{ range := λ a b, char.of_nat <$> (a.to_nat .. b.to_nat) }
#eval 'a'..'z'
#eval 'A'..'z'
#eval 10..20
#eval 1..2
```

#### Eric Wieser (Feb 18 2021 at 15:53):

I think docs#list.range' is a better match for your `has_range ℕ`

#### Eric Wieser (Feb 18 2021 at 15:55):

I've updated my comment above with a link to the branch I'm thinking of. Here's a definition basically equal to your `has_range`

#### Kana (Feb 18 2021 at 16:00):

Hm, is mathlib something like community stdlib now? I have only default lean lib, with init.data.list without range'.

#### Yakov Pechersky (Feb 18 2021 at 16:02):

```
import data.equiv.basic
class has_range (α : Type*) :=
(range : α → α → list α)
infix `..`:50 := has_range.range
def has_range.of_equiv {α : Type*} (e : α ≃ ℕ) : has_range α :=
⟨λ x y, list.map e.symm $ list.range' (e x) (e y - e x)⟩
instance : has_range ℕ := has_range.of_equiv (equiv.refl _)
instance : has_range char :=
{ range := λ a b, char.of_nat <$> (a.to_nat .. b.to_nat) }
#eval 'a'..'z'
#eval 'A'..'z'
#eval 10..20
#eval 1..2
```

#### Mario Carneiro (Feb 18 2021 at 21:07):

@kana Yes, there isn't really anything called stdlib in lean 3, there is the core library in the lean repo and then there is mathlib, and for the most part all of us on zulip are going to assume you have mathlib (it's a monorepo development style)

#### Mario Carneiro (Feb 18 2021 at 21:08):

the core library is intentionally minimal, so I would recommend you use mathlib for operations on lists and such, like list.range'

#### Mario Carneiro (Feb 18 2021 at 21:09):

The reason why `list.range'`

takes a start and length instead of start and end is because the latter makes the implicit assumption that the start is less or equal to the end, and this complicates proofs and reasoning about the function

Last updated: Dec 20 2023 at 11:08 UTC