pattern matching with zero cases

Stream: lean4

[rambip]

Hi !
As I was reading "induction and recursion" in the book, I found the "dependant pattern matching" part pretty hard to understand.
I have two questions:
1) is it possible to have a pattern-matching with zero cases, to make the compiler understand it is an impossible situation (to prove 0 != 1 for example) ?
2) what is Nat.noConfusion, I cannot find any explanation on that topic
Thanks in advance

[Reid Barton]

Re 2, there is https://xenaproject.wordpress.com/2018/03/24/no-confusion-over-no_confusion/

[Reid Barton]

(Written for Lean 3, but it should be essentially the same in Lean 4)

[rambip]

Thanks !
It would be so usefull to explain that (at least the goal of noConfusion) in the doc !

[Kyle Miller]

Re 1, yes, the zero-case version of match is called nomatch:

example (h : 0 = 1) : false := nomatch h

(This is doing cases on Eq, and it's able to see that h can't be rfl so there are no other cases.)

[Ryan McCorvie]

@Reid Barton Thanks for this reference. TPIL4 and the lean reference manual are a little sparse in terms of explaining noConfusion