no_confusion proofs

Stream: general

[Gihan Marasingha]

I see that some proofs (e.g. nat.not_succ_le_zero) are simply a dot. The full proof term clearly uses no_confusion.

My question are: how is . turned into a proof term? What can . prove? Is this documented somewhere?

[Mario Carneiro]

It is a 0-ary pattern match

[Mario Carneiro]

the term is produced by the equation compiler