From 8f49d3d89784095089bf0885268b4e87e2fbc69c Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Tue, 24 Feb 2015 11:03:02 -0500
Subject: [PATCH] add a small demo for lean mode

---
 demo/kitchen-sink/docs/lean.lean | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 demo/kitchen-sink/docs/lean.lean

diff --git a/demo/kitchen-sink/docs/lean.lean b/demo/kitchen-sink/docs/lean.lean
new file mode 100644
index 00000000..40e82753
--- /dev/null
+++ b/demo/kitchen-sink/docs/lean.lean
@@ -0,0 +1,9 @@
+import logic
+section
+  variables (A : Type) (p q : A → Prop)
+
+  example : (∀x : A, p x ∧ q x) → ∀y : A, p y  :=
+  assume H : ∀x : A, p x ∧ q x,
+  take y : A,
+  show p y, from and.elim_left (H y)
+end