match loses something

Stream: new members

[A.]

I'm a little surprised that this doesn't just work*

def last {α : Type} (a : Array α) : Option α :=
  match a.size with
  | 0 => none
  | m + 1 => some a[m]

The match docstring says

If used as match h : e, ... with | p, ... => f | ..., h : e = p is available within f.

What am I missing?

[Markus Himmel]

You need to give a name to the hypothesis:

def last {α : Type} (a : Array α) : Option α :=
  match h : a.size with
  | 0 => none
  | m + 1 => some a[m]

[A.]

Thanks!