Trigger CI for https://github.com/leanprover/lean4/pull/3110 #62258
leanprover-community-mathlib4-botbuild.yml
on: push
Cancel Previous Runs (CI)
3s
check workflows
10s
Post-CI job
0s
Annotations
10 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
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
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
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/Tactic/FailIfNoProgress.lean#L60
The function definition has 2 extra paramters, but 3 variables are bound here. Bind exactly 2 variables here!
|
|
Build:
Mathlib/Tactic/FailIfNoProgress.lean#L60
too many variable names
|
|
Build:
Mathlib/Tactic/SuppressCompilation.lean#L31
unexpected token '?'; expected ')'
|
|
Build:
Mathlib/Tactic/SuppressCompilation.lean#L32
unexpected doc string
|
|
Build:
Mathlib/Tactic/SuppressCompilation.lean#L33
elaboration function for 'command.pseudo.antiquot' has not been implemented
|
|
Build:
Mathlib/Tactic/SuppressCompilation.lean#L33
unexpected token '?'; expected command
|