t ::= -- term x -- variable fun x: T. t -- abstraction t t -- application fun2 X. t -- type abstraction t [T] -- type application T ::= X -- type variable T -> T -- arrow type (for abstractions) forall X. T -- universal type (for type abstractions) 

Variable X; -- assumes type variable X Axiom x: T; -- assumes variable x: T (synonym: Hypothesis) Define x = t; -- defines x = t Theorem x: T = t; -- checks t has a type T and defines x = t (synonyms: Lemma, Corollary) Reduce t; -- performs full beta-reduction on t Print x; -- prints term bound to x Clear; -- clears the context 

> Variable False; False is assumed. > Axiom ex: forall X. False -> X; ex: forall X. False -> X is assumed. > Axiom dne: forall X. ((X -> False) -> False) -> X; dne: forall X. ((X -> False) -> False) -> X is assumed. > Theorem peirce: forall A, B. ((A -> B) -> A) -> A | = fun2 A. | fun2 B. | dne [((A -> B) -> A) -> A] ( | fun H: (((A -> B) -> A) -> A) -> False. | H ( | fun H0: (A -> B) -> A. | H0 ( | fun H1: A. | ex [B] ( | H ( | fun H2: (A -> B) -> A. | H1 | ) | ) | ) | ) | ); peirce: forall A. forall B. ((A -> B) -> A) -> A is defined. > Print peirce; peirce: forall A. forall B. ((A -> B) -> A) -> A = fun2 A. fun2 B. dne [((A -> B) -> A) -> A] (fun H: (((A -> B) -> A) -> A) -> False. H (fun H0: (A -> B) -> A. H0 (fun H1: A. ex [B] (H (fun H2: (A -> B) -> A. H1))))) > Clear; > Print peirce; Reference Error at (line 1, column 1): unbound variable: peirce > Define s = fun2 A, B, C. fun x: A -> B -> C, y : A -> B, z : A. x z (y z); s: forall A. forall B. forall C. (A -> B -> C) -> (A -> B) -> A -> C is defined. > Define k = fun2 A, B. fun x: A, y : B. x; k: forall A. forall B. A -> B -> A is defined. > Define i = fun2 A. fun x: A. x; i: forall A. A -> A is defined. > Reduce fun2 X. fun x: X. s [X] [X] [X] (k [X] [X]) (i [X]) x; fun2 A. fun a: A. a