Skip to content

Commit

Permalink
Update test output
Browse files Browse the repository at this point in the history
  • Loading branch information
nomeata committed Feb 26, 2024
1 parent 0409e0b commit 4f62d9b
Show file tree
Hide file tree
Showing 2 changed files with 9 additions and 9 deletions.
16 changes: 8 additions & 8 deletions tests/lean/guessLexFailures.lean.expected.out
Original file line number Diff line number Diff line change
Expand Up @@ -40,23 +40,23 @@ The arguments relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
x1 x2 x3
1) 29:6-25 = = =
2) 30:6-23 = ? <
2) 30:6-23 = < _
3) 31:6-23 < _ _
Please use `termination_by` to specify a decreasing measure.
guessLexFailures.lean:37:0-43:31: error: Could not find a decreasing measure.
The arguments relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
x1 x2 x3 x4
1) 39:6-27 = = _ =
2) 40:6-25 = ? _ <
2) 40:6-25 = < _ _
3) 41:6-25 < _ _ _
Please use `termination_by` to specify a decreasing measure.
guessLexFailures.lean:48:0-54:31: error: Could not find a decreasing measure.
The arguments relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
n m l
1) 50:6-25 = = =
2) 51:6-23 = ? <
2) 51:6-23 = < _
3) 52:6-23 < _ _
Please use `termination_by` to specify a decreasing measure.
guessLexFailures.lean:59:6-59:7: error: fail to show termination for
Expand All @@ -74,16 +74,16 @@ Call from Mutual.f to Mutual.f at 61:8-33:
= = =
Call from Mutual.f to Mutual.f at 62:8-31:
n m l
= ? <
= < <
Call from Mutual.f to Mutual.g at 63:8-39:
n m l
n < _ ?
m ? _ ?
n < ? ?
m ? = ?
H _ _ _
l ? _ <
l ? ? <
Call from Mutual.g to Mutual.g at 68:8-35:
n m H l
? _ _ =
? ? _ =
Call from Mutual.g to Mutual.g at 69:8-33:
n m H l
_ _ _ <
Expand Down
2 changes: 1 addition & 1 deletion tests/lean/wf1.lean.expected.out
Original file line number Diff line number Diff line change
Expand Up @@ -15,5 +15,5 @@ Could not find a decreasing measure.
The arguments relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
x y
1) 3:12-19 ? ?
1) 3:12-19 ?
Please use `termination_by` to specify a decreasing measure.

0 comments on commit 4f62d9b

Please sign in to comment.