Trigger CI for https://github.com/leanprover/lean4/pull/3040 #62203
Annotations
4 errors
|
build mathlib
The function definition has no extra parameters, so `termination_by` should not bind any. Variables bound in the function header can be referred directly.
|
|
build mathlib
fail to show termination for
|
|
build mathlib
unused `termination_by`, function is not recursive
|
|
build mathlib
The process '/usr/bin/bash' failed with exit code 1
|
The logs for this run have expired and are no longer available.
Loading