range

Stream: new members

[Kana]

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]

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

[Yakov Pechersky]

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

[Kana]

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]

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

[Eric Wieser]

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]

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

[Yakov Pechersky]

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]

@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]

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

[Mario Carneiro]

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