LambdaPiPlus
Try!
About
Syntax
Prelude
--A proof that x >= y is a a natural z, --paired with a proof that z + y = x let geq = (\ x y -> exists (z :: Nat) . Eq _ x (plus y z) ) :: Nat -> Nat -> * --Any Natural number is geq to 0 let geq0 = (\n -> (n , p0PlusNisN _) ) :: forall (n :: Nat ) . geq n 0 --A proof that there is a number greater than any given natural number let natsAreInf = (\n -> (Succ n, (0, symm _ (plus (Succ n) 0) (Succ n) (pNPlus0isN _)) ) ) :: forall (n :: Nat) . exists (m :: Nat) . gt m n
TypeCheck Program