Zulip Chat Archive

Stream: new members

Topic: syntax help

Matt Diamond (Jun 21 2021 at 02:42):

I was reading through the implementation of Cantor's diagonal argument (specifically the theorem cantor_surjective) and I was having trouble understanding some of the syntax. For instance: the return type appears to be ¬ function.surjective f | h... what is the | character doing? Is this pattern matching? When stepping through the code, I noticed that h has the type function.surjective f, but I'm not sure how that assignment was made.

Alex J. Best (Jun 21 2021 at 02:49):

The type not P is exactly P -> false so to prove such a theorem we can pattern match on h of type P and give a proof of false constructed from h after the :=

Matt Diamond (Jun 21 2021 at 02:50):

Ah, that makes sense... thanks!

Last updated: Dec 20 2023 at 11:08 UTC