Skip to content

Commit 0491229

Browse files
committed
perf(DoldKan/EquivalencePseudoabelian): use suppress_compilation (#13858)
Compiling the file takes 14s; the computability is not used anywhere in mathlib. Speeds up the file by 78%.
1 parent e743f36 commit 0491229

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

Mathlib/AlgebraicTopology/DoldKan/EquivalencePseudoabelian.lean

+2
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ Authors: Joël Riou
66
import Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive
77
import Mathlib.AlgebraicTopology.DoldKan.Compatibility
88
import Mathlib.CategoryTheory.Idempotents.SimplicialObject
9+
import Mathlib.Tactic.SuppressCompilation
910

1011
#align_import algebraic_topology.dold_kan.equivalence_pseudoabelian from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
1112

@@ -35,6 +36,7 @@ the composition of `N₁ : SimplicialObject C ⥤ Karoubi (ChainComplex C ℕ)`
3536
-/
3637

3738

39+
suppress_compilation
3840
noncomputable section
3941

4042
open CategoryTheory CategoryTheory.Category CategoryTheory.Limits CategoryTheory.Idempotents

0 commit comments

Comments
 (0)