18c97926a1
this is in preparation for #4542, and extracts from `findRecArg` the functionality for trying one particular argument. It also refactors the code a bit. In particular * It reports errors in the order of the parameters, not the order of in which they are tried (it tries non-indices first). * For every argument it will say why it wasn't tried, even if the reason is quite obviously (fixed prefix, or `Prop`-typed etc.) Therefore there is some error message churn.
19 lines
619 B
Text
19 lines
619 B
Text
wf1.lean:1:4-1:5: error: fail to show termination for
|
|
g
|
|
with errors
|
|
structural recursion cannot be used:
|
|
|
|
argument #1 cannot be used for structural recursion
|
|
failed to eliminate recursive application
|
|
g (x - 1)
|
|
|
|
argument #2 cannot be used for structural recursion
|
|
insufficient number of parameters at recursive application
|
|
g (x - 1)
|
|
|
|
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 y - x
|
|
1) 3:12-19 ≤ ? ?
|
|
Please use `termination_by` to specify a decreasing measure.
|