ffbea840bf
If here is only one plausible measure, there is no point having the `GuessLex` code see if it is terminating, running all the tactics, only for the `MkFix` code then run the tactics again. So if there is only one plausible measure (non-mutual recursion with only one varying parameter), just use that measure. Side benefit: If the function isn’t terminating, more detailed error messages are shown (failing proof goals), located at the recursive calls.
17 lines
880 B
Text
17 lines
880 B
Text
guessLexFailures.lean:11:12-11:46: error: fail to show termination for
|
|
nonTerminating
|
|
with errors
|
|
argument #1 was not used for structural recursion
|
|
failed to eliminate recursive application
|
|
nonTerminating (Nat.succ n) (Nat.succ m)
|
|
|
|
argument #2 was not used for structural recursion
|
|
failed to eliminate recursive application
|
|
nonTerminating (Nat.succ n) (Nat.succ m)
|
|
|
|
structural recursion cannot be used
|
|
|
|
failed to prove termination, use `termination_by` to specify a well-founded relation
|
|
guessLexFailures.lean:15:0-18:31: error: failed to prove termination, use `termination_by` to specify a well-founded relation
|
|
guessLexFailures.lean:25:0-27:31: error: failed to prove termination, use `termination_by` to specify a well-founded relation
|
|
guessLexFailures.lean:33:0-36:31: error: failed to prove termination, use `termination_by` to specify a well-founded relation
|