# Zulip Chat Archive

## 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'

was my answer.

#### 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