Move lean stuff in its own folder

mk12 · Dec 25, 2018 · 7490873 · 7490873
1 parent 598a5dc
commit 7490873
Show file tree

Hide file tree

Showing 4 changed files with 19 additions and 0 deletions.
diff --git a/src/chapter_2.lean → lean/src/chapter_2.lean b/src/chapter_2.lean → lean/src/chapter_2.lean
diff --git a/src/chapter_3.lean → lean/src/chapter_3.lean b/src/chapter_3.lean → lean/src/chapter_3.lean
diff --git a/src/common.lean → lean/src/common.lean b/src/common.lean → lean/src/common.lean
diff --git a/lean/src/test.lean b/lean/src/test.lean
@@ -0,0 +1,19 @@
+import standard
+open eq.ops
+open nat classical set
+check sigma.
+
+  -- Axiom of specification for Mem
+  -- section specification
+  --   parameters {X : Set} (P : Mem X → Prop)
+
+  --   definition specify_mem : Set :=
+  --     λ x, x ∈ X ∧ ∀ Hx : x ∈ X, P (Mem.mk Hx)
+
+  --   definition specify_mem_subset : specify_mem ⊆ X :=
+  --     take x,
+  --     suppose x ∈ specify_mem,
+  --     show x ∈ X, from and.left this
+  -- end specification
+check trivial
+find_decl (_ → (_ → _))