indexed with fin n

Stream: general

[Logan Murphy]

I've been going over the documentation but I'm having some trouble writing simple concrete tuples using fin n as index type (trying to avoid using vectors). I feel like I should be able to write something like the following

def silly : fin 2 → bool := λ i, match i with
| ⟨0,_⟩ := ff
| ⟨1,_⟩ := tt
end

Lean wants an additional case

⟨(nat.succ _).succ, _⟩

If fin 2 is a type with two elements, each being a nat with evidence that this nat is less than two, what is the third case trying to account for?

[Mario Carneiro]

the third case can be proved impossible, but lean can't show it immediately

[Mario Carneiro]

You should use fin.cons to construct functions like this

[Yakov Pechersky]

You can also do tt for 0 and ff for the rest

[Kenny Lau]

import data.fin2
import data.matrix.notation

open fin2

def silly : fin2 2 → bool
| fz      := ff
| (fs fz) := tt

def silly' : fin 2 → bool :=
![ff, tt]

#eval silly fz      -- ff
#eval silly (fs fz) -- tt
#eval silly' 0      -- ff
#eval silly' 1      -- tt