Skip to content

Commit dff9eb8

Browse files
committed
'fix' tests
1 parent d8fe6c0 commit dff9eb8

File tree

3 files changed

+2
-6
lines changed

3 files changed

+2
-6
lines changed

test/Mathlib/test/20240209.expected.out

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
{"env": 0}
2-
31
{"sorries":
42
[{"proofState": 0,
53
"pos": {"line": 1, "column": 22},
@@ -10,7 +8,7 @@
108
"pos": {"line": 1, "column": 0},
119
"endPos": {"line": 1, "column": 7},
1210
"data": "declaration uses 'sorry'"}],
13-
"env": 1}
11+
"env": 0}
1412

1513
{"proofState": 1,
1614
"messages":

test/Mathlib/test/20240209.in

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
{"cmd": "import Std.Tactic.Simpa"}
2-
3-
{"cmd": "example : False := by sorry", "env": 0}
1+
{"cmd": "example : False := by sorry"}
42

53
{"tactic": "simpa using show False by done", "proofState": 0}

0 commit comments

Comments
 (0)