Probably a bug

Stream: lean4

[Uranus Testing]

How does this work (version 4.0.0, commit 56cd6c1ff519, Release)?

inductive A : Type
| ctor : A → A
| inh

def f : A → A → Bool
| banana, a b | _, lol how => 1 + "test" + f1
| _, _ => false

[Henrik Böving]

If you #print f you can see what the elaborator makes out of it, its basically ignoring the first two matches and only uses the false branch. This seem like a bug in the elaborator to me indeed.

[Sébastien Michelland]

The syntax seems a bit tricky, if you avoid having two cases on the same line by repeating the first => you get a full error.

[Uranus Testing]

So it seems that problem is somewhere in the implementation of these “or” patterns.
This reminds me about similar in some sense bug in cubicaltt.

[Leonardo de Moura]

@Uranus Testing Thanks for raising this issue. I pushed a fix for it.
https://github.com/leanprover/lean4/commit/dca8a8ed98cebc5e8d338a3a38e154859759b4c4