Zulip Chat Archive

Stream: general

Topic: no_confusion proofs


Gihan Marasingha (May 07 2021 at 13:03):

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 (May 07 2021 at 13:03):

It is a 0-ary pattern match

Mario Carneiro (May 07 2021 at 13:03):

the term is produced by the equation compiler


Last updated: Dec 20 2023 at 11:08 UTC