diff --git a/tests/lean/traceTacticSteps.lean b/tests/lean/traceTacticSteps.lean
new file mode 100644
index 0000000000..2c677dc841
--- /dev/null
+++ b/tests/lean/traceTacticSteps.lean
@@ -0,0 +1,8 @@
+-- Check whether all intermediate steps during tactic execution
+-- can be successfully pretty-printed to trace output
+
+set_option trace.Elab.step true
+
+example : True := by
+  skip
+  trivial
diff --git a/tests/lean/traceTacticSteps.lean.expected.out b/tests/lean/traceTacticSteps.lean.expected.out
new file mode 100644
index 0000000000..d850644bbc
--- /dev/null
+++ b/tests/lean/traceTacticSteps.lean.expected.out
@@ -0,0 +1,44 @@
+[Elab.step] expected type: Sort ?u, term
+True
+[Elab.step] expected type: True, term
+by 
+  skip 
+  trivial
+[Elab.step] 
+  skip 
+  trivial
+[Elab.step] 
+  skip 
+  trivial
+[Elab.step] skip
+[Elab.step] trivial
+[Elab.step] (apply And.intro✝) <;> trivial
+[Elab.step] focus 
+  (
+    apply And.intro✝;
+    all_goals 
+      trivial)
+[Elab.step] 
+  (
+    apply And.intro✝;
+    all_goals 
+      trivial)
+[Elab.step] 
+  (
+    apply And.intro✝;
+    all_goals 
+      trivial)
+[Elab.step] (
+  apply And.intro✝;
+  all_goals 
+    trivial)
+[Elab.step] 
+  apply And.intro✝;
+  all_goals 
+    trivial
+[Elab.step] 
+  apply And.intro✝;
+  all_goals 
+    trivial
+[Elab.step] apply And.intro✝
+[Elab.step] apply True.intro✝