f36bbc8d56
The previous check, looking only at the type of the parameter, was too permissive and led to ill-typed terms later on. This fixes #4671. In some cases the previous code might have worked by accident, in this sense this is a breaking change. Affected functions can be fixed by reordering their parameters to that all the function parameters that occur in the parameter of the inductive type of the parameter that the function recurses on come first.
21 lines
544 B
Text
21 lines
544 B
Text
set_option linter.constructorNameAsVariable false
|
|
|
|
inductive A (n : Nat) : Type
|
|
| a : A n
|
|
| b : A n → A n
|
|
|
|
/--
|
|
error: argument #3 cannot be used for structural recursion
|
|
its type is an inductive datatype
|
|
A n
|
|
and the datatype parameter
|
|
n
|
|
depends on the function parameter
|
|
n
|
|
which does not come before the varying parameters and before the indices of the recursion parameter.
|
|
-/
|
|
#guard_msgs in
|
|
def A.size (acc n : Nat) : A n → Nat
|
|
| .a => acc
|
|
| .b a' => 1 + A.size (acc + 1) n a'
|
|
termination_by structural a => a
|