testing the typechecker

alt="Your browser isn't running the applet, for some reason." Your browser is ignoring the <APPLET> tag!

Here's an example which should typecheck:

{
absurd = !p:#. p;
truth = !p:#. p -> p;
not = \p:#. p -> absurd;
and = \p:#. \q:#. !c:#. p -> (q -> c);
or = \p:#. \q:#. !c:#. (p -> c) -> ((q -> c) -> c);
implies = \p:#. \q:#. p -> q;

id = \t:#. \x:t. x;
Bool_cases = { t:#; true:t; false:t; };
Bool = !c:Bool_cases. c.t;
Bool_true = \c:Bool_cases. c.true;
Bool_false = \c:Bool_cases. c.false;

Nat_cases = { t:#; zero:t; succ: t->t; };
Nat = !c:Nat_cases. c.t;
zero = \c:Nat_cases. c.zero;
one = \c:Nat_cases. c.succ c.zero;
two = \c:Nat_cases. c.succ (c.succ c.zero);
}