iterating over `Fin n`

Stream: lean4

[Adam Topaz]

What's the Lean4 idiomatic way to accomplish this?

def go : IO Unit := do
  for i in Fin 5 do
    IO.println i

[František Silváši 🦉]

I would do:

def go : IO Unit := do
  for i in [:5] do
    IO.println i

[Adam Topaz]

well sure, but Fin 5 includes proofs that the naturals are less than 5.

[Adam Topaz]

And I would like to use them in the body of the for loop

[Adam Topaz]

There is a nice trick of doing
for h : i in [:5] do ...
and h can be used to get such a proof, but it would be nice to be able to iterate over Fin n directly

[Adam Topaz]

I.e. something like this

def go : IO Unit := do
  for h : i in [:5] do
    let j : Fin 5 := ⟨i, h.2⟩
    IO.println j

[František Silváši 🦉]

Sorry I misunderstood your question, I thought you wanted something to the tune of having a Fin 5 there, not specifically getting the Fin 5 thing to work.

[Mario Carneiro]

Unfortunately the ToStream class is not dependent, otherwise I think we could just have made your original code do the right thing

[Mario Carneiro]

We can do this though:

structure Upto (n : Nat)
def upto (n) : Upto n where

instance : ForIn m (Upto n) (Fin n) where
  forIn _ x f := forIn' [:n] x fun i h x => f ⟨i, by exact h.2⟩ x

def go : IO Unit := do
  for i in upto 5 do
    IO.println i

[Frédéric Dupuis]

(deleted)