From ec38e652a7545e8d6bee9b941dbdbe62700f32d2 Mon Sep 17 00:00:00 2001
From: "William J. Bowman" <wjb@williamjbowman.com>
Date: Mon, 19 Jan 2015 13:15:16 -0500
Subject: [PATCH] Started modeling STLC

---
 example.rkt | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

diff --git a/example.rkt b/example.rkt
index 657b55d..17038ab 100644
--- a/example.rkt
+++ b/example.rkt
@@ -236,3 +236,30 @@
      (inhabit-type (forall (a : (-> true true))
                    (forall (f : (and true true))
                    true))))
+
+;; -------------------
+;; Okay but what about *real* proofs, like formalizing STLC, complete
+;; with fancy syntax for type checking?
+
+(data type : Type
+  (Unit : type)
+  (Pair : (->* type type type))
+  (Fun  : (->* type type type)))
+
+(data var : Type
+  (v : (-> nat var)))
+
+(data term : Type
+  (tvar : (-> var term))
+  (unitv : term)
+  (pair  : (->* term term term))
+  (lam   : (->* var type term term))
+  (prj   : (->* nat term term))
+  (app   : (->* term term term)))
+
+(define-syntax (λ syn)
+  (syntax-case syn (:)
+    [(_ (x : t) e)
+     #'(lam (v x) t e)]))
+
+(check-equal? (lam (v z) Unit unitv) (λ (z : Unit) unitv))