6 lines
159 B
Text
6 lines
159 B
Text
283.lean:1:4-1:5: error: fail to show termination for
|
|
f
|
|
with errors
|
|
structural recursion cannot be used
|
|
|
|
well founded recursion has not been implemented yet
|