chore: add test

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

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✝