add more tests (leanprover-community#18)

Author: kim-em

test/Mathlib/test/H20231115.expected.out

@@ -0,0 +1,19 @@
+{"env": 0}
+
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 36},
+   "goal": "x : Nat ⊢ x + 1 > x",
+   "endPos": {"line": 1, "column": 41}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 0},
+   "endPos": {"line": 1, "column": 7},
+   "data": "declaration uses 'sorry'"}],
+ "env": 1}
+
+{"proofState": 1,
+ "goals":
+ ["case zero\n⊢ Nat.zero + 1 > Nat.zero",
+  "case succ\nx : Nat\nhx : x + 1 > x\n⊢ Nat.succ x + 1 > Nat.succ x"]}
+

test/Mathlib/test/H20231115.in

@@ -0,0 +1,5 @@
+{"cmd": "import Mathlib.Tactic.Cases"}
+
+{"cmd": "example {x : Nat} : x + 1 > x := by sorry", "env": 0}
+
+{"tactic": "induction' x with x hx", "proofState": 0}

test/Mathlib/test/H20231115_2.expected.out

@@ -0,0 +1,18 @@
+{"env": 0}
+
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 3, "column": 12},
+   "goal": "case zero ⊢ Nat.zero + 1 > Nat.zero",
+   "endPos": {"line": 3, "column": 17}},
+  {"proofState": 1,
+   "pos": {"line": 3, "column": 12},
+   "goal": "case succ x : Nat hx : x + 1 > x ⊢ Nat.succ x + 1 > Nat.succ x",
+   "endPos": {"line": 3, "column": 17}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 0},
+   "endPos": {"line": 1, "column": 7},
+   "data": "declaration uses 'sorry'"}],
+ "env": 1}
+

test/Mathlib/test/H20231115_2.in

@@ -0,0 +1,4 @@
+{"cmd": "import Mathlib.Tactic.Cases"}
+
+{"cmd": "example {x : Nat} : x + 1 > x := by\n  induction' x with x hx\n  all_goals sorry", "env": 0}
+

test/Mathlib/test/H20231115_3.expected.out

@@ -0,0 +1,10 @@
+{"env": 0}
+
+{"messages":
+ [{"severity": "error",
+   "pos": {"line": 1, "column": 33},
+   "endPos": {"line": 2, "column": 24},
+   "data":
+   "unsolved goals\ncase zero\n⊢ Nat.zero + 1 > Nat.zero\n\ncase succ\nx : Nat\nhx : x + 1 > x\n⊢ Nat.succ x + 1 > Nat.succ x"}],
+ "env": 1}
+

test/Mathlib/test/H20231115_3.in

@@ -0,0 +1,4 @@
+{"cmd": "import Mathlib.Tactic.Cases"}
+
+{"cmd": "example {x : Nat} : x + 1 > x := by\n  induction' x with x hx", "env": 0}
+