Permalink
Browse files

Added README

  • Loading branch information...
1 parent 1235d47 commit bfdb2c2d6a12f431cee2a21b9439a6f957ae1ce8 @andrejbauer andrejbauer committed Nov 5, 2012
Showing with 28 additions and 0 deletions.
  1. +28 −0 README.markdown
View
@@ -0,0 +1,28 @@
+A minimalist implementation of type theory with universes indexed by numerals and
+dependent products. The concrete syntax is as follows:
+
+* The universes are `Type 0`, `Type 1`, `Type 2`, ...
+* A dependent product is written as `forall x : T1, T2`
+* A function is written as `fun x : T => e`
+* Application is written as `e1 e2`
+
+Type `Help.` in the interactive shell to see what the type system can do. Here is a sample
+session:
+
+ Type Ctrl-D to exit or "Help." for help.]
+ # Parameter nat : Type 0.
+ nat is assumed
+ # Parameter z : nat.
+ z is assumed
+ # Parameter s : nat -> nat.
+ s is assumed
+ # Eval (fun f : nat -> nat => fun n : nat => f (f (f (f n)))) (fun n : nat => s (s (s n))) (s (s (s (s z)))).
+ = s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s z)))))))))))))))
+ : nat
+ # Check (fun A : Type 0 => fun f : A -> Type 1 => fun a : A => f A).
+ Typing error: type mismatch
+ # Check (fun A : Type 0 => fun f : A -> Type 1 => fun a : A => f a).
+ fun A : Type 0 => fun f : A -> Type 1 => fun a : A => f a
+ : forall A : Type 0, (A -> Type 1) -> A -> Type 1
+
+

0 comments on commit bfdb2c2

Please sign in to comment.