add more tests

leanprover-community · Nov 14, 2023 · 7a8a99e · 7a8a99e
1 parent 0ddd89e
commit 7a8a99e
Show file tree

Hide file tree

Showing 6 changed files with 60 additions and 0 deletions.
diff --git a/test/Mathlib/test/H20231115.expected.out b/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"]}
+
diff --git a/test/Mathlib/test/H20231115.in b/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}
diff --git a/test/Mathlib/test/H20231115_2.expected.out b/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}
+
diff --git a/test/Mathlib/test/H20231115_2.in b/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}
+
diff --git a/test/Mathlib/test/H20231115_3.expected.out b/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}
+
diff --git a/test/Mathlib/test/H20231115_3.in b/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}
+
Original file line number	Diff line number	Diff line change
		@@ -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}