test using on_goal

Author: kim-em

test/Mathlib/test/on_goal.expected.out

@@ -0,0 +1,22 @@
+{"env": 0}
+
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 60},
+   "goal": "x : ℝ\nh0 : |x| > 1\n⊢ x < 0 ∨ 2 * x > 2",
+   "endPos": {"line": 1, "column": 65}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 0},
+   "endPos": {"line": 1, "column": 7},
+   "data": "declaration uses 'sorry'"}],
+ "env": 1}
+
+{"sorries":
+ [{"proofState": 1, "goal": "x : ℝ\nh0 : |x| > 1\n⊢ x = x"},
+  {"proofState": 2, "goal": "x : ℝ\nh0 : |x| > 1\nh1 : x = x\n⊢ x = x"}],
+ "proofState": 3,
+ "goals":
+ ["case pos\nx : ℝ\nh0 : |x| > 1\nh1 h2 : x = x\nh3 : x < 0\n⊢ x < 0 ∨ 2 * x > 2",
+  "case neg\nx : ℝ\nh0 : |x| > 1\nh1 h2 : x = x\nh3 : ¬x < 0\n⊢ x < 0 ∨ 2 * x > 2"]}
+

test/Mathlib/test/on_goal.in

@@ -0,0 +1,5 @@
+{"cmd": "import Mathlib\nopen Real"}
+
+{"cmd": "example {x : ℝ} (h0: |x| > 1) : (x < 0) ∨ (2 * x > 2) := by sorry", "env": 0}
+
+{"tactic": "on_goal 1 =>\n  have h1 : x = x := by sorry\n  have h2 : x = x := by sorry\n  by_cases h3 : x < 0", "proofState": 0}