Trigger CI for https://github.com/leanprover/lean4/pull/3121 #66247
leanprover-community-mathlib4-botbuild.yml
on: push
Cancel Previous Runs (CI)
4s
check workflows
7s
Post-CI job
0s
Annotations
10 errors
|
Build
'Lean.PrettyPrinter.Delaborator.withOverApp' has already been declared
|
|
Build
Too many extra parameters bound; the function definition only has 0 extra parameters.
|
|
Build
Too many extra parameters bound; the function definition only has 0 extra parameters.
|
|
Build
Too many extra parameters bound; the function definition only has 0 extra parameters.
|
|
Build
Too many extra parameters bound; the function definition only has 0 extra parameters.
|
|
Build
function expected at
|
|
Build
missing cases:
|
|
Build
fields missing: 'simprocs'
|
|
Build
Too many extra parameters bound; the function definition only has 5 extra parameters.
|
|
Build
missing cases:
|