syntax help

Stream: new members

[Matt Diamond]

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]

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]

Ah, that makes sense... thanks!