delete Lemmas.lean
#165362
JovanGerbAnnotations
1 error and 8 warnings
|
Build
The process '/usr/bin/env' failed with exit code 1
|
|
Build:
Mathlib/Logic/IsEmpty.lean#L8
unused import (use `lake exe shake --fix` to fix this, or `lake exe shake --update` to ignore)
|
|
Build:
Mathlib/Logic/IsEmpty.lean#L8
import #[Mathlib.Tactic.Push.Basic] instead
|
|
Build:
Mathlib/Order/Defs/LinearOrder.lean#L11
unused import (use `lake exe shake --fix` to fix this, or `lake exe shake --update` to ignore)
|
|
Build:
Mathlib/Logic/Nontrivial/Defs.lean#L8
unused import (use `lake exe shake --fix` to fix this, or `lake exe shake --update` to ignore)
|
|
Build:
Mathlib/Tactic/Contrapose.lean#L7
unused import (use `lake exe shake --fix` to fix this, or `lake exe shake --update` to ignore)
|
|
Build:
Mathlib/Tactic/Contrapose.lean#L7
import #[Mathlib.Logic.Basic] instead
|
|
Build:
Mathlib/Data/Nat/Defs.lean#L11
unused import (use `lake exe shake --fix` to fix this, or `lake exe shake --update` to ignore)
|
|
Build:
Mathlib/Tactic/ByContra.lean#L7
unused import (use `lake exe shake --fix` to fix this, or `lake exe shake --update` to ignore)
|
Artifacts
Produced during runtime
| Name | Size | |
|---|---|---|
|
import-graph
|
198 KB |
|