More refactoring

Signed-off-by: Sky Wilshaw <[email protected]>
leanprover-community · Dec 5, 2024 · 39c33b4 · 39c33b4
1 parent 62ba28f
commit 39c33b4
Show file tree

Hide file tree

Showing 19 changed files with 29 additions and 29 deletions.
diff --git a/ConNF.lean b/ConNF.lean
@@ -12,15 +12,8 @@ import ConNF.Base.BasePerm
 import ConNF.Base.Litter
 import ConNF.Base.NearLitter
 import ConNF.Base.Params
-import ConNF.Base.Position
 import ConNF.Base.Small
 import ConNF.Base.TypeIndex
-import ConNF.Coherent.CoherentData
-import ConNF.Coherent.Enumeration
-import ConNF.Coherent.Fuzz
-import ConNF.Coherent.ModelData
-import ConNF.Coherent.PathEnumeration
-import ConNF.Coherent.Support
 import ConNF.Construction.Code
 import ConNF.Construction.NewModelData
 import ConNF.Counting.BaseCoding
@@ -39,9 +32,6 @@ import ConNF.FOA.StrAction
 import ConNF.FOA.StrActionFOA
 import ConNF.FOA.StrApprox
 import ConNF.FOA.StrApproxFOA
-import ConNF.Levels.BasePositions
-import ConNF.Levels.Deny
-import ConNF.Levels.Level
 import ConNF.Levels.Path
 import ConNF.Levels.StrPerm
 import ConNF.Levels.StrSet
@@ -55,6 +45,16 @@ import ConNF.Model.RaiseStrong
 import ConNF.Model.Result
 import ConNF.Model.RunInduction
 import ConNF.Model.TTT
+import ConNF.ModelData.CoherentData
+import ConNF.ModelData.Enumeration
+import ConNF.ModelData.Fuzz
+import ConNF.ModelData.Level
+import ConNF.ModelData.ModelData
+import ConNF.ModelData.PathEnumeration
+import ConNF.ModelData.Support
+import ConNF.Position.BasePositions
+import ConNF.Position.Deny
+import ConNF.Position.Position
 import ConNF.Strong.SMulSpec
 import ConNF.Strong.Spec
 import ConNF.Strong.SpecSame

diff --git a/ConNF/Construction/Code.lean b/ConNF/Construction/Code.lean
@@ -1,4 +1,4 @@
-import ConNF.Coherent.CoherentData
+import ConNF.ModelData.CoherentData
 
 /-!
 # Codes

diff --git a/ConNF/Counting/CodingFunction.lean b/ConNF/Counting/CodingFunction.lean
@@ -1,4 +1,4 @@
-import ConNF.Coherent.CoherentData
+import ConNF.ModelData.CoherentData
 
 /-!
 # Coding functions

diff --git a/ConNF/Counting/Twist.lean b/ConNF/Counting/Twist.lean
@@ -1,4 +1,4 @@
-import ConNF.Coherent.ModelData
+import ConNF.ModelData.ModelData
 
 /-!
 # Twisting sets

diff --git a/ConNF/FOA/BaseApprox.lean b/ConNF/FOA/BaseApprox.lean
@@ -1,4 +1,4 @@
-import ConNF.Coherent.Support
+import ConNF.ModelData.Support
 import ConNF.FOA.Coherent
 
 /-!

diff --git a/ConNF/FOA/Coherent.lean b/ConNF/FOA/Coherent.lean
@@ -1,4 +1,4 @@
-import ConNF.Coherent.CoherentData
+import ConNF.ModelData.CoherentData
 import ConNF.FOA.Inflexible
 
 /-!

diff --git a/ConNF/FOA/Inflexible.lean b/ConNF/FOA/Inflexible.lean
@@ -1,4 +1,4 @@
-import ConNF.Coherent.CoherentData
+import ConNF.ModelData.CoherentData
 
 /-!
 # New file

diff --git a/ConNF/FOA/StrApprox.lean b/ConNF/FOA/StrApprox.lean
@@ -1,4 +1,4 @@
-import ConNF.Coherent.CoherentData
+import ConNF.ModelData.CoherentData
 import ConNF.FOA.BaseApprox
 
 /-!

diff --git a/ConNF/Model/InductionStatement.lean b/ConNF/Model/InductionStatement.lean
@@ -1,4 +1,4 @@
-import ConNF.Coherent.CoherentData
+import ConNF.ModelData.CoherentData
 import ConNF.Construction.Code
 
 /-!

diff --git a/ConNF/Coherent/CoherentData.lean → ConNF/ModelData/CoherentData.lean b/ConNF/Coherent/CoherentData.lean → ConNF/ModelData/CoherentData.lean
@@ -1,6 +1,6 @@
-import ConNF.Coherent.Fuzz
-import ConNF.Levels.Level
-import ConNF.Coherent.ModelData
+import ConNF.ModelData.Fuzz
+import ConNF.ModelData.Level
+import ConNF.ModelData.ModelData
 
 /-!
 # Coherent data
@@ -9,7 +9,7 @@ In this file, we define the type of coherent data below a particular proper type
 
 ## Main declarations
 
-* `ConNF.CoherentData`: Coherent data below a given level `α`.
+* `ConNF.ModelDataData`: Coherent data below a given level `α`.
 -/
 
 noncomputable section

diff --git a/ConNF/Coherent/Enumeration.lean → ConNF/ModelData/Enumeration.lean b/ConNF/Coherent/Enumeration.lean → ConNF/ModelData/Enumeration.lean
diff --git a/ConNF/Coherent/Fuzz.lean → ConNF/ModelData/Fuzz.lean b/ConNF/Coherent/Fuzz.lean → ConNF/ModelData/Fuzz.lean
@@ -1,5 +1,5 @@
-import ConNF.Levels.BasePositions
-import ConNF.Coherent.ModelData
+import ConNF.Position.BasePositions
+import ConNF.ModelData.ModelData
 
 /-!
 # The `fuzz` map

diff --git a/ConNF/Levels/Level.lean → ConNF/ModelData/Level.lean b/ConNF/Levels/Level.lean → ConNF/ModelData/Level.lean
diff --git a/ConNF/Coherent/ModelData.lean → ConNF/ModelData/ModelData.lean b/ConNF/Coherent/ModelData.lean → ConNF/ModelData/ModelData.lean
@@ -1,5 +1,5 @@
 import ConNF.Levels.StrSet
-import ConNF.Coherent.Support
+import ConNF.ModelData.Support
 
 /-!
 # Model data

diff --git a/ConNF/Coherent/PathEnumeration.lean → ConNF/ModelData/PathEnumeration.lean b/ConNF/Coherent/PathEnumeration.lean → ConNF/ModelData/PathEnumeration.lean
@@ -1,4 +1,4 @@
-import ConNF.Coherent.Enumeration
+import ConNF.ModelData.Enumeration
 import ConNF.Levels.StrPerm
 
 /-!

diff --git a/ConNF/Coherent/Support.lean → ConNF/ModelData/Support.lean b/ConNF/Coherent/Support.lean → ConNF/ModelData/Support.lean
@@ -1,4 +1,4 @@
-import ConNF.Coherent.PathEnumeration
+import ConNF.ModelData.PathEnumeration
 
 /-!
 # Supports

diff --git a/ConNF/Levels/BasePositions.lean → ConNF/Position/BasePositions.lean b/ConNF/Levels/BasePositions.lean → ConNF/Position/BasePositions.lean
@@ -1,4 +1,4 @@
-import ConNF.Levels.Deny
+import ConNF.Position.Deny
 import ConNF.Base.NearLitter
 
 /-!

diff --git a/ConNF/Levels/Deny.lean → ConNF/Position/Deny.lean b/ConNF/Levels/Deny.lean → ConNF/Position/Deny.lean
@@ -1,4 +1,4 @@
-import ConNF.Base.Position
+import ConNF.Position.Position
 
 /-!
 # Injective functions from denied sets

diff --git a/ConNF/Base/Position.lean → ConNF/Position/Position.lean b/ConNF/Base/Position.lean → ConNF/Position/Position.lean