Structured Proof Script LanguageΒΆ

Harpoon proofs are recorded in signature files as a proof script. This is a structured language whose core constructs close resembles the syntax of Proof tactics. In a signature file, a proof named foo is declared as follows.

proof foo : tau = P;

where tau is a computation type and P is the body of the proof.