Anonymous hypothesis works with if, but not with match.

Stream: lean4

[MrQubo]

This works:

def last {α : Type} (a : Array α) : Option α :=
  if _ : a.size = 0
    then none
    else some a[a.size-1]

but this doesn't:

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

although using e.g. h instead of _ works in both. Shouldn't match support anonymous hypothesis as well?

[Henrik Böving]

I think that should work yes, could you open an issue?

[MrQubo]

I wanted to, but I couldn't find where is the place to report issues with lean. I've tried to find it on https://lean-lang.org/ and https://leanprover-community.github.io/ but no luck.

[Henrik Böving]

https://github.com/leanprover/lean4

[MrQubo]

Thanks! I've made an issue https://github.com/leanprover/lean4/issues/6759.