test(tests/lean): When and Cond tactical tests

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

tests/lean/cond_tac.lean

@@ -0,0 +1,45 @@
+import tactic
+(*
+simple_tac = Cond(function(env, ios, s)
+                     local gs = s:goals()
+                     local n, g = gs:head()
+                     local r = g:conclusion():is_and()
+                     print ("Cond result: " .. tostring(r))
+                     return r
+                  end,
+                  Then(apply_tac("and_intro"), assumption_tac()),
+                  Then(apply_tac("or_introl"), assumption_tac()))
+
+simple2_tac = When(function(env, ios, s)
+                      local gs = s:goals()
+                      local n, g = gs:head()
+                      local r = g:conclusion():is_and()
+                      print ("When result: " .. tostring(r))
+                      return r
+                   end,
+                   apply_tac("and_intro"))
+*)
+theorem T1 (a b c : Bool) : a -> b -> c -> a ∧ b.
+  (* simple_tac *)
+  done
+
+theorem T2 (a b : Bool) : a -> a ∨ b.
+  (* simple_tac *)
+  done
+
+definition x := 10
+theorem T3 : x + 20 +2 >= 2*x.
+  (* eval_tac() *)
+  (* trivial_tac() *)
+  done
+
+theorem T4 (a b c : Bool) : a -> b -> c -> a ∧ b.
+  (* simple2_tac *)
+  exact
+  done
+
+theorem T5 (a b c : Bool) : a -> b -> c -> a ∨ b.
+  (* simple2_tac *)
+  apply or_introl
+  exact
+  done

tests/lean/cond_tac.lean.expected.out

@@ -0,0 +1,13 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Imported 'tactic'
+Cond result: true
+  Proved: T1
+Cond result: false
+  Proved: T2
+  Defined: x
+  Proved: T3
+When result: true
+  Proved: T4
+When result: false
+  Proved: T5