test(tests/lean/run): add some 'lost' tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

tests/lean/run/booltst.lean

@@ -0,0 +1,4 @@
+import standard
+using bool
+
+check '0

tests/lean/run/bug5.lean

@@ -0,0 +1,4 @@
+import standard
+
+theorem symm2 {A : Type} {a b : A} (H : a = b) : b = a
+:= subst H (refl a)

tests/lean/run/goal.lean

@@ -0,0 +1,5 @@
+import standard
+using tactic
+
+theorem T {a b c d : Prop} (H : a) (H : b) (H : c) (H : d) : a
+:= by state; assumption

tests/lean/run/set.lean

@@ -0,0 +1,7 @@
+import standard bool
+using bool
+
+definition set {{T : Type}} := T → bool
+infix `∈`:50 := λx A, A x = '1
+
+check 1 ∈ (λ x, '1)

tests/lean/run/set2.lean

@@ -0,0 +1,18 @@
+import standard bool
+using bool
+
+namespace set
+
+definition set (T : Type) := T → bool
+definition mem {T : Type} (a : T) (s : set T) := s a = '1
+infix `∈`:50 := mem
+
+section
+  parameter {T : Type}
+
+  definition empty : set T := λx, '0
+  notation `∅` := empty
+
+  theorem mem_empty (x : T) : ¬ (x ∈ ∅)
+  := not_intro (λH : x ∈ ∅, absurd H b0_ne_b1)
+end