the errors are getting interesting #64457
kim-embuild.yml
on: push
Cancel Previous Runs (CI)
5s
check workflows
7s
Post-CI job
0s
Annotations
12 errors
|
Lint style:
Mathlib/Tactic/SimpIntro.lean#L69
Mathlib/Tactic/SimpIntro.lean#L69: ERR_LIN: Line has more than 100 characters
|
|
Lint style
Process completed with exit code 123.
|
|
Build:
Mathlib/Control/Traversable/Lemmas.lean#L107
tactic 'simp' failed, nested error:
|
|
Build:
Mathlib/Tactic/FieldSimp.lean#L74
overloaded, errors
|
|
Build:
Mathlib/Tactic/FieldSimp.lean#L73
invalid constructor ⟨...⟩, expected type must be an inductive type
|
|
Build:
Mathlib/Tactic/FieldSimp.lean#L178
invalid dotted identifier notation, unknown identifier `Lean.Meta.Simp.Simprocs.simp` from expected type
|
|
Build:
Mathlib/Tactic/FieldSimp.lean#L190
application type mismatch
|
|
Build:
Mathlib/Tactic/FieldSimp.lean#L179
invalid field notation, type is not of the form (C ...) where C is a constant
|
|
Build:
Mathlib/Tactic/FieldSimp.lean#L181
invalid field notation, type is not of the form (C ...) where C is a constant
|
|
Build:
Mathlib/Tactic/FieldSimp.lean#L182
invalid field notation, type is not of the form (C ...) where C is a constant
|
|
Build:
Mathlib/Tactic/FieldSimp.lean#L185
invalid field notation, type is not of the form (C ...) where C is a constant
|
|
Build:
Mathlib/Tactic/FieldSimp.lean#L186
invalid field notation, type is not of the form (C ...) where C is a constant
|