Trigger CI for https://github.com/leanprover/lean4/pull/3040 #62203
leanprover-community-mathlib4-botbuild.yml
on: push
Cancel Previous Runs (CI)
4s
check workflows
11s
Post-CI job
0s
Annotations
4 errors
|
Build
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
fail to show termination for
|
|
Build
unused `termination_by`, function is not recursive
|
|
Build
The process '/usr/bin/bash' failed with exit code 1
|