Zulip Chat Archive

Stream: new members

Topic: range


view this post on Zulip 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

view this post on Zulip Eric Wieser (Feb 18 2021 at 15:30):

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

view this post on Zulip Yakov Pechersky (Feb 18 2021 at 15:42):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Feb 18 2021 at 15:53):

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

view this post on Zulip 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

view this post on Zulip 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'.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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'

view this post on Zulip 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: May 15 2021 at 23:13 UTC