diff --git a/tests/lean/run/meta3.lean b/tests/lean/run/meta3.lean
new file mode 100644
index 0000000000..256de735ac
--- /dev/null
+++ b/tests/lean/run/meta3.lean
@@ -0,0 +1,5 @@
+open name
+
+check "foo" <s> "bla"
+
+vm_eval "foo" <s> "bla" <n> 10 <n> 20
diff --git a/tests/lean/run/meta_tac2.lean b/tests/lean/run/meta_tac2.lean
new file mode 100644
index 0000000000..a01d1095bc
--- /dev/null
+++ b/tests/lean/run/meta_tac2.lean
@@ -0,0 +1,56 @@
+set_option pp.all true
+
+open tactic name list
+
+set_option pp.goal.compact true
+set_option pp.binder_types true
+
+#tactic (∀ (p : Prop), p → p → p),
+ do
+    intro_lst ["_", "H1", "H2"],
+    revert "H1",
+    trace_state,
+    r ← result,
+    trace_expr r,
+    intro "H3",
+    r ← result,
+    trace_expr r,
+    assumption,
+    r ← result,
+    trace_expr r,
+    return ()
+
+print "====================="
+
+#tactic (∀ (p : Prop), p → p → p),
+ do
+    intro_lst ["_", "H1", "H2"],
+    revert_lst ["H1", "H2"],
+    trace_state,
+    r ← result,
+    trace_expr r,
+    intro "H3",
+    trace_state,
+    trace "------------",
+    r ← result,
+    trace_expr r,
+    (assumption <|> trace "assumption failed"),
+    intro "H4",
+    assumption,
+    trace "------------",
+    r ← result,
+    trace_expr r,
+    return ()
+
+print "====================="
+
+#tactic (∀ (p : Prop), p → p → p),
+ do
+   intros,
+   revert "p",
+   trace_state,
+   intros,
+   assumption,
+   r ← result,
+   trace_expr r,
+   return ()