curry-howard

Slides of a (very) informal lecture of mine on the Curry-Howard correspondence

Diffstat

5 files changed, 22 insertions, 18 deletions

diff --git a/examples/eq.lean b/examples/eq.lean
@@ -1,4 +1,4 @@
-inductive Eq (x : t) (y : t) : Prop
-| rfl : Eq x x
+inductive eq (x : t) (y : t) : Prop
+| rfl : eq x x
 
-infix = := Eq
+infix = := eq

diff --git a/examples/example.lean b/examples/example.lean
@@ -1,9 +1,7 @@
-lemma ex : Or p q → Or q p := by
+lemma ex : or p q → or q p := by
   intro h
   match h with
-  | Or.inl _  =>
-    apply Or.inr
-    assumption
-  | Or.inr h2 =>
-    apply Or.inl
-    exact h2
+  | inl h1 =>
+    exact inr h1
+  | inr h1 =>
+    exact inl h1

diff --git a/examples/liquid.lean b/examples/liquid.lean
@@ -0,0 +1,6 @@
+variables (p' p : ℝ≥0) 
+  [fact (0 < p')] [fact (p' < p)] [fact (p ≤ 1)]
+
+theorem liquid_tensor_experiment 
+  (S : Profinite) (V : pBanach p) :
+  ∀ i > 0, Ext i (M_{p'} S) V ≅ 0 :=

diff --git a/examples/nat.lean b/examples/nat.lean
@@ -1,3 +1,3 @@
-inductive Nat : Type 
-| zero : Nat
-| succ : Nat → Nat
+inductive ℕ : Type
+| zero : ℕ
+| succ : ℕ → ℕ

diff --git a/examples/types.lean b/examples/types.lean
@@ -1,7 +1,7 @@
 -- a e b <-> And a b
-inductive And (a : Prop) (b : Prop) : Prop
-| intro : a → b → And a b
+inductive and (a : Prop) (b : Prop) : Prop
+| intro : a → b → and a b
 
-inductive Or (a : Prop) (b : Prop) : Prop
-| inl : a → Or a b
-| inr : b → Or a b
+inductive or (a : Prop) (b : Prop) : Prop
+| inl : a → or a b
+| inr : b → or a b