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.
16 lines
997 B
Text
16 lines
997 B
Text
sanitychecks.lean:1:8-1:15: error: fail to show termination for
|
|
unsound
|
|
with errors
|
|
structural recursion cannot be used:
|
|
|
|
well-founded recursion cannot be used, 'unsound' does not take any (non-fixed) arguments
|
|
sanitychecks.lean:4:8-4:32: error: 'partial' theorems are not allowed, 'partial' is a code generation directive
|
|
sanitychecks.lean:7:7-7:31: error: 'unsafe' theorems are not allowed
|
|
sanitychecks.lean:10:0-10:23: error: failed to synthesize
|
|
Inhabited False
|
|
use `set_option diagnostics true` to get diagnostic information
|
|
sanitychecks.lean:18:12-18:20: error: invalid use of 'partial', 'Foo.unsound3' is not a function
|
|
False
|
|
sanitychecks.lean:20:0-20:54: error: failed to compile partial definition 'Foo.unsound4', failed to show that type is inhabited and non empty
|
|
sanitychecks.lean:22:12-22:20: error: (kernel) invalid declaration, it uses unsafe declaration 'unsafeCast'
|
|
sanitychecks.lean:25:12-25:20: error: (kernel) invalid declaration, it uses unsafe declaration 'unsafeCast'
|