Add test example

Author: augustepoiroux

test/Mathlib/test/incrementality.expected.out

@@ -0,0 +1,68 @@
+{"tactics":
+ [{"usedConstants":
+   ["Nat.gcd",
+    "HMul.hMul",
+    "Mathlib.Meta.NormNum.isNat_eq_true",
+    "instMulNat",
+    "instOfNatNat",
+    "Mathlib.Meta.NormNum.isNat_ofNat",
+    "Tactic.NormNum.nat_gcd_helper_2",
+    "Nat.instAddMonoidWithOne",
+    "Nat",
+    "Eq.refl",
+    "Mathlib.Meta.NormNum.instAddMonoidWithOneNat",
+    "Tactic.NormNum.isNat_gcd",
+    "OfNat.ofNat",
+    "instHMul"],
+   "tactic": "norm_num",
+   "proofState": 0,
+   "pos": {"line": 2, "column": 60},
+   "goals": "⊢ Nat.gcd 180 168 = 12",
+   "endPos": {"line": 2, "column": 68}},
+  {"usedConstants": ["Eq.refl"],
+   "tactic": "rfl",
+   "proofState": 1,
+   "pos": {"line": 10, "column": 2},
+   "goals": "α✝ : Sort u_1\nn : α✝\n⊢ n = n",
+   "endPos": {"line": 10, "column": 5}}],
+ "messages":
+ [{"severity": "info",
+   "pos": {"line": 8, "column": 0},
+   "endPos": {"line": 8, "column": 5},
+   "data": "9227465"}],
+ "env": 0}
+
+{"tactics":
+ [{"usedConstants":
+   ["Nat.gcd",
+    "HMul.hMul",
+    "Mathlib.Meta.NormNum.isNat_eq_true",
+    "instMulNat",
+    "instOfNatNat",
+    "Mathlib.Meta.NormNum.isNat_ofNat",
+    "Tactic.NormNum.nat_gcd_helper_2",
+    "Nat.instAddMonoidWithOne",
+    "Nat",
+    "Eq.refl",
+    "Mathlib.Meta.NormNum.instAddMonoidWithOneNat",
+    "Tactic.NormNum.isNat_gcd",
+    "OfNat.ofNat",
+    "instHMul"],
+   "tactic": "norm_num",
+   "proofState": 2,
+   "pos": {"line": 2, "column": 60},
+   "goals": "⊢ Nat.gcd 180 168 = 12",
+   "endPos": {"line": 2, "column": 68}},
+  {"usedConstants": ["Nat", "Eq.refl"],
+   "tactic": "rfl",
+   "proofState": 3,
+   "pos": {"line": 10, "column": 2},
+   "goals": "n : ℕ\n⊢ n = n + 0",
+   "endPos": {"line": 10, "column": 5}}],
+ "messages":
+ [{"severity": "info",
+   "pos": {"line": 8, "column": 0},
+   "endPos": {"line": 8, "column": 5},
+   "data": "9227465"}],
+ "env": 1}
+

test/Mathlib/test/incrementality.in

@@ -0,0 +1,3 @@
+{"cmd": "import Mathlib\ntheorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num\ndef fib : Nat → Nat\n  | 0 => 0\n  | 1 => 1\n  | n + 2 => fib (n + 1) + fib n\n\n#eval fib 35\ntheorem foo : n = n := by\n  rfl", "allTactics": true}
+
+{"cmd": "import Mathlib\ntheorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num\ndef fib : Nat → Nat\n  | 0 => 0\n  | 1 => 1\n  | n + 2 => fib (n + 1) + fib n\n\n#eval fib 35\ntheorem foo2 : n = n+0 := by\n  rfl", "allTactics": true}