Trigger CI for https://github.com/leanprover/lean4/pull/3124 #63477
leanprover-community-mathlib4-botbuild.yml
on: push
Cancel Previous Runs (CI)
2s
check workflows
8s
Post-CI job
0s
Annotations
10 errors
|
Build:
Mathlib/Tactic/SimpIntro.lean#L24
application type mismatch
|
|
Build:
Mathlib/Tactic/SimpIntro.lean#L39
application type mismatch
|
|
Build:
Mathlib/Tactic/SimpIntro.lean#L68
fields missing: 'simprocs'
|
|
Build
function expected at
|
|
Build:
Mathlib/Util/DischargerAsTactic.lean#L25
typeclass instance problem is stuck, it is often due to metavariables
|
|
Build
function expected at
|
|
Build
application type mismatch
|
|
Build
invalid constructor ⟨...⟩, expected type must be an inductive type
|
|
Build
missing cases:
|
|
Build
fields missing: 'simprocs'
|