Skip to content

Commit d4d965c

Browse files
Update incrementality test
1 parent 9fb52d5 commit d4d965c

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

test/Mathlib/test/incrementality.in

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
{"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}
1+
{"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, "incrementality": true}
22

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 foo2 : n = n+0 := by\n rfl", "allTactics": true}
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 foo2 : n = n+0 := by\n rfl", "allTactics": true, "incrementality": true}
44

5-
{"cmd": "import Mathlib\n-- comment to test if header is reused even when a comment is added"}
5+
{"cmd": "import Mathlib\n-- comment to test if header is reused even when a comment is added", "incrementality": true}

0 commit comments

Comments
 (0)