add some test cases

test/Mathlib/test/induction.expected.out

@@ -0,0 +1,29 @@
+{"env": 0}
+
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 36},
+   "goal": "x : ℕ\n⊢ x = x",
+   "endPos": {"line": 1, "column": 41}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 11},
+   "data": "declaration uses 'sorry'"}],
+ "env": 1}
+
+{"proofState": 1,
+ "goals":
+ ["case zero\n⊢ Nat.zero = Nat.zero",
+  "case succ\nn✝ : ℕ\nn_ih✝ : n✝ = n✝\n⊢ Nat.succ n✝ = Nat.succ n✝"]}
+
+{"proofState": 2,
+ "goals": ["case succ\nn✝ : ℕ\nn_ih✝ : n✝ = n✝\n⊢ Nat.succ n✝ = Nat.succ n✝"]}
+
+{"sorries":
+ [{"proofState": 3, "goal": "case zero\n⊢ Nat.zero = Nat.zero"},
+  {"proofState": 4,
+   "goal": "case succ\nx : ℕ\nn_ih✝ : x = x\n⊢ Nat.succ x = Nat.succ x"}],
+ "proofState": 5,
+ "goals": []}
+

test/Mathlib/test/induction.in

@@ -0,0 +1,10 @@
+{"cmd": "import Mathlib"}
+
+{"env" : 0, "cmd": "theorem foo (x : Nat) : x = x := by sorry"}
+
+{"proofState" : 0, "tactic": "induction x"}
+
+{"proofState" : 1, "tactic": "next => rfl"}
+
+{"proofState" : 0, "tactic": "induction x with\n| zero => sorry\n| succ x => sorry"}
+

test/Mathlib/test/induction.lean

@@ -0,0 +1,6 @@
+import Mathlib
+
+theorem bar (x : Nat) : x = x := by
+  induction x with
+  | zero => sorry
+  | succ n ih => sorry

test/by_cases.expected.out

@@ -0,0 +1,19 @@
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 36},
+   "goal": "x : Int\n⊢ x = x",
+   "endPos": {"line": 1, "column": 41}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 11},
+   "data": "declaration uses 'sorry'"}],
+ "env": 0}
+
+{"proofState": 1,
+ "goals":
+ ["case inl\nx : Int\nh : x < 0\n⊢ x = x",
+  "case inr\nx : Int\nh : ¬x < 0\n⊢ x = x"]}
+
+{"proofState": 2, "goals": ["case inr\nx : Int\nh : ¬x < 0\n⊢ x = x"]}
+

test/by_cases.in

@@ -0,0 +1,6 @@
+{"cmd": "theorem foo (x : Int) : x = x := by sorry"}
+
+{"proofState" : 0, "tactic": "by_cases h : x < 0"}
+
+{"proofState" : 1, "tactic": "case inl => rfl"}
+

test/by_cases.lean

@@ -0,0 +1,4 @@
+theorem foo (x : Int) : x = x := by
+  by_cases h : x < 0
+  next => rfl
+  next => rfl