The Curry-Howard Correspondence¶

Proof Scripts¶

Quantifiers, Implications, Functions¶

Programming with Tactics¶

Logical Connectives as Inductive Types¶

Conjunction¶

Disjunction¶

Existential Quantification¶

True and False¶

Equality¶

Inversion, Again¶