## Stream: general

### Topic: vector exercise from Leroy's lectures

#### Kevin Buzzard (Jun 28 2019 at 09:13):

inductive xfin : ℕ → Type
| zero : ∀ n, xfin (nat.succ n)
| succ : ∀ n, xfin n → xfin (nat.succ n)

inductive vec (A : Type) : ℕ → Type
| nil : vec 0
| cons : ∀ n, A → vec n → vec (nat.succ n)

def mth (A : Type) (n : ℕ) (v : vec A n) (m : xfin n) : A := sorry


Slightly trickier than I expected, but I got there in the end. Returns the m'th element of the vector.

#### Kevin Buzzard (Jun 28 2019 at 09:21):

Unit tests:

#eval mth ℕ 2 (vec.cons 1 4 (vec.cons 0 6 (vec.nil ℕ))) (xfin.zero 1) -- 4
#eval mth ℕ 2 (vec.cons 1 4 (vec.cons 0 6 (vec.nil ℕ))) (xfin.succ 1 (xfin.zero 0)) -- 6


#### Mario Carneiro (Jun 28 2019 at 09:47):

def mth (A : Type) : ∀ (n : ℕ), vec A n → xfin n → A
| _ (vec.cons n a l) (xfin.zero _) := a
| _ (vec.cons _ a l) (xfin.succ n i) := mth n l i


#### Kevin Buzzard (Jun 28 2019 at 11:00):

Damn you Carneiro, I needed four lines :-)

#### Kevin Buzzard (Jun 28 2019 at 11:01):

Oh wait -- your answer is better than mine: I needed to use ._ (I think). Unfortunately my answer is at home right now.

#### Koundinya Vajjha (Jun 28 2019 at 11:08):

I'm surprised while writing this you didn't cause lean to segfault. I faced the same problem a few days ago.
https://github.com/leanprover-community/lean/issues/52

#### Kevin Buzzard (Jun 29 2019 at 21:35):

def mth (A : Type) : Π (n : ℕ) (v : vec A n) (m : xfin n), A
| 0 v m := by cases m
| (d+1) (vec.cons ._ a w) (xfin.zero ._) := a
| (d+1) (vec.cons ._ a w) (xfin.succ ._ e') := mth d w e'


#### Kenny Lau (Jun 30 2019 at 08:40):

I think you can omit the second line

#### Kevin Buzzard (Jun 30 2019 at 18:16):

Right -- the equation compiler is smart enough to do the cases, it seems.

#### Kevin Buzzard (Jun 30 2019 at 18:19):

def mth (A : Type) : Π (n : ℕ) (v : vec A n) (m : xfin n), A
| _ (vec.cons _ a _) (xfin.zero _) := a
| _ (vec.cons _ _ w) (xfin.succ _ e') := mth _ w e'


I think that's the sup of what you can omit

#### Mario Carneiro (Jun 30 2019 at 18:20):

The ._ inaccessible patterns seem to be optional now, ever since leo made some change to the way the equation compiler handles these things

#### Mario Carneiro (Jun 30 2019 at 18:21):

which is useful since it's hard to know how to use them properly

Last updated: May 15 2021 at 23:13 UTC