From: Chris Barker <barker@omega.(none)>
Date: Mon, 25 Oct 2010 02:35:25 +0000 (-0400)
Subject: added Curry-Howard
X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=0bdafef1c31c5372b1b7d5a960e2a016754d5388;hp=8e8edc03022be0da1621d6f1b418919c2637856e

added Curry-Howard
---

diff --git a/week6.mdwn b/week6.mdwn
index 57158c6b..f26285f3 100644
--- a/week6.mdwn
+++ b/week6.mdwn
@@ -261,26 +261,26 @@ Axiom: -----------
 
 Structural Rules:
 
-Exchange: &Gamma;, x:A, y:B, &Delta; |- R:C
-          -------------------------------
+          &Gamma;, x:A, y:B, &Delta; |- R:C
+Exchange: -------------------------------
           &Gamma;, y:B, x:A, &Delta; |- R:C
 
-Contraction: &Gamma;, x:A, x:A |- R:B
-             --------------------------
+             &Gamma;, x:A, x:A |- R:B
+Contraction: --------------------------
              &Gamma;, x:A |- R:B
 
-Weakening: &Gamma; |- R:B
-           --------------------- 
+           &Gamma; |- R:B
+Weakening: --------------------- 
            &Gamma;, x:A |- R:B     [x chosen fresh]
 
 Logical Rules:
 
---> I:   &Gamma;, x:A |- R:B
-         -------------------------
+         &Gamma;, x:A |- R:B
+--> I:   -------------------------
          &Gamma; |- \xM:A --> B  
 
---> E:   &Gamma; |- f:(A --> B)      &Gamma; |- x:A
-         -------------------------------------
+         &Gamma; |- f:(A --> B)      &Gamma; |- x:A
+--> E:   -------------------------------------
          &Gamma; |- (fx):B
 </pre>