List of consequtive Fin like List.Ico

Stream: Is there code for X?

[Naruyoko]

docs#List.Ico gives a list of consecutive naturals. Given a ≤ b ≤ c, is there an equivalent to List.Ico a b but with type List (Fin c)?

[Eric Wieser]

You can use Finset.Ico, but obviously that won't be a list:

import Mathlib

-- {1, 2, 3}
#eval Finset.Ico (1 : Fin 5) (9 : Fin 5)

[Edward van de Meent]

docs#List.finRange is a thing, you can probably start looking there...

[Edward van de Meent]

@loogle |- List (Fin ?_)

[loogle]

:search: Fin.list, List.finRange

[Edward van de Meent]

it would appear that's about everything we have...

[Edward van de Meent]

but you could certainly take inspiration from their definitions to make what you need

[Eric Wieser]

I guess you also need to watch out for the case when b = c, since then (b : Fin c) = 0

[Naruyoko]

The definition of docs#List.finRange looks promising.

[Naruyoko]

I got the following:

import Mathlib.Data.List.Intervals

def finIco {k : ℕ} (m n : Fin (k + 1)) : List (Fin k) :=
  (List.Ico m n).pmap Fin.mk fun _ h =>
    Nat.lt_of_lt_of_le (List.Ico.mem.mp h).right (Nat.le_of_lt_succ n.isLt)

#reduce finIco (k := 3) 0 2
#reduce finIco (k := 3) 1 3
#reduce finIco (k := 3) 2 2
#reduce finIco (k := 3) 3 2