## Stream: general

### Topic: indexed with fin n

#### Logan Murphy (Aug 14 2020 at 02:34):

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


⟨(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 (Aug 14 2020 at 02:37):

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

#### Mario Carneiro (Aug 14 2020 at 02:37):

You should use fin.cons to construct functions like this

#### Yakov Pechersky (Aug 14 2020 at 02:41):

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

#### Kenny Lau (Aug 14 2020 at 05:07):

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


Last updated: May 10 2021 at 18:22 UTC