remove empty & deprecated modules

forked-from-1kasper · Oct 16, 2024 · b1ff44c · b1ff44c
1 parent 164dcb7
commit b1ff44c
Show file tree

Hide file tree

Showing 4 changed files with 645 additions and 706 deletions.
diff --git a/GroundZero.lean b/GroundZero.lean
@@ -51,10 +51,8 @@ import GroundZero.HITs.Pushout
 import GroundZero.HITs.Quotient
 import GroundZero.HITs.Reals
 import GroundZero.HITs.Setquot
-import GroundZero.HITs.Simplicial
 import GroundZero.HITs.Sphere
 import GroundZero.HITs.Suspension
-import GroundZero.HITs.Topologization
 import GroundZero.HITs.Trunc
 import GroundZero.HITs.Wedge
 import GroundZero.Meta.Basic

diff --git a/GroundZero/HITs/Simplicial.lean b/GroundZero/HITs/Simplicial.lean
diff --git a/GroundZero/HITs/Topologization.lean b/GroundZero/HITs/Topologization.lean