Skip to content

Commit

Permalink
Refactor initial construction structure
Browse files Browse the repository at this point in the history 
Signed-off-by: zeramorphic <[email protected]>
  • Loading branch information
@zeramorphic
zeramorphic committed Dec 3, 2024
1 parent 6fdc87c commit 8896e41
Show file tree
Hide file tree
Showing 44 changed files with 86 additions and 86 deletions.
2 changes: 1 addition & 1 deletion .vscode/con-nf.code-snippets
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@
"scope": "lean4",
"prefix": "newfile",
"body": [
"import ConNF.Setup.Params",
"import ConNF.Base.Params",
"",
"/-!",
"# New file",
Expand Down
62 changes: 31 additions & 31 deletions ConNF.lean
View file
Original file line number Diff line number Diff line change
@@ -1,12 +1,24 @@
import ConNF.Basic.Cardinal
import ConNF.Basic.InductiveConstruction
import ConNF.Basic.Ordinal
import ConNF.Basic.PermutativeExtension
import ConNF.Basic.ReflTransGen
import ConNF.Basic.Rel
import ConNF.Basic.Set
import ConNF.Basic.Transfer
import ConNF.Basic.WellOrder
import ConNF.Background.Cardinal
import ConNF.Background.InductiveConstruction
import ConNF.Background.Ordinal
import ConNF.Background.PermutativeExtension
import ConNF.Background.ReflTransGen
import ConNF.Background.Rel
import ConNF.Background.Set
import ConNF.Background.Transfer
import ConNF.Background.WellOrder
import ConNF.Base.Atom
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.Fuzz
import ConNF.Coherent.ModelData
import ConNF.Coherent.Support
import ConNF.Construction.Code
import ConNF.Construction.NewModelData
import ConNF.Counting.BaseCoding
Expand All @@ -15,7 +27,6 @@ import ConNF.Counting.CodingFunction
import ConNF.Counting.Conclusions
import ConNF.Counting.CountSupportOrbit
import ConNF.Counting.Recode
import ConNF.Counting.Strong
import ConNF.Counting.Twist
import ConNF.FOA.BaseAction
import ConNF.FOA.BaseApprox
Expand All @@ -26,6 +37,15 @@ 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.Coherent.Enumeration
import ConNF.Levels.Level
import ConNF.Levels.Path
import ConNF.Coherent.PathEnumeration
import ConNF.Levels.StrPerm
import ConNF.Levels.StrSet
import ConNF.Levels.Tree
import ConNF.Model.ConstructHypothesis
import ConNF.Model.ConstructMotive
import ConNF.Model.Externalise
Expand All @@ -35,27 +55,7 @@ import ConNF.Model.RaiseStrong
import ConNF.Model.Result
import ConNF.Model.RunInduction
import ConNF.Model.TTT
import ConNF.Setup.Atom
import ConNF.Setup.BasePerm
import ConNF.Setup.BasePositions
import ConNF.Setup.CoherentData
import ConNF.Setup.Deny
import ConNF.Setup.Enumeration
import ConNF.Setup.Fuzz
import ConNF.Setup.Level
import ConNF.Setup.Litter
import ConNF.Setup.ModelData
import ConNF.Setup.NearLitter
import ConNF.Setup.Params
import ConNF.Setup.Path
import ConNF.Setup.PathEnumeration
import ConNF.Setup.Position
import ConNF.Setup.Small
import ConNF.Setup.StrPerm
import ConNF.Setup.StrSet
import ConNF.Setup.Support
import ConNF.Setup.Tree
import ConNF.Setup.TypeIndex
import ConNF.Strong.SMulSpec
import ConNF.Strong.Spec
import ConNF.Strong.SpecSame
import ConNF.Strong.Strong
2 changes: 1 addition & 1 deletion ConNF/Basic/Cardinal.lean → ConNF/Background/Cardinal.lean
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
import Mathlib.SetTheory.Cardinal.Cofinality
import ConNF.Basic.Rel
import ConNF.Background.Rel

universe u v

Expand Down
0 ConNF/Basic/InductiveConstruction.lean → ConNF/Background/InductiveConstruction.lean
View file
File renamed without changes.
2 changes: 1 addition & 1 deletion ConNF/Basic/Ordinal.lean → ConNF/Background/Ordinal.lean
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import ConNF.Basic.WellOrder
import ConNF.Background.WellOrder
import Mathlib.SetTheory.Cardinal.Aleph
import Mathlib.SetTheory.Cardinal.Arithmetic

Expand Down
4 changes: 2 additions & 2 deletions ConNF/Basic/PermutativeExtension.lean → ConNF/Background/PermutativeExtension.lean
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
import ConNF.Basic.Cardinal
import ConNF.Basic.Rel
import ConNF.Background.Cardinal
import ConNF.Background.Rel

noncomputable section
open Cardinal
Expand Down
4 changes: 2 additions & 2 deletions ConNF/Basic/ReflTransGen.lean → ConNF/Background/ReflTransGen.lean
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
import ConNF.Basic.Cardinal
import ConNF.Basic.Rel
import ConNF.Background.Cardinal
import ConNF.Background.Rel

universe u

Expand Down
0 ConNF/Basic/Rel.lean → ConNF/Background/Rel.lean
View file
File renamed without changes.
0 ConNF/Basic/Set.lean → ConNF/Background/Set.lean
View file
File renamed without changes.
2 changes: 1 addition & 1 deletion ConNF/Basic/Transfer.lean → ConNF/Background/Transfer.lean
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
import Mathlib.Logic.Equiv.TransferInstance
import ConNF.Basic.Ordinal
import ConNF.Background.Ordinal

universe u v

Expand Down
0 ConNF/Basic/WellOrder.lean → ConNF/Background/WellOrder.lean
View file
File renamed without changes.
4 changes: 2 additions & 2 deletions ConNF/Setup/Atom.lean → ConNF/Base/Atom.lean
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
import ConNF.Setup.Litter
import ConNF.Setup.Small
import ConNF.Base.Litter
import ConNF.Base.Small

/-!
# Atoms
Expand Down
2 changes: 1 addition & 1 deletion ConNF/Setup/BasePerm.lean → ConNF/Base/BasePerm.lean
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
import Mathlib.Logic.Equiv.Defs
import ConNF.Setup.NearLitter
import ConNF.Base.NearLitter

/-!
# Base permutations
Expand Down
2 changes: 1 addition & 1 deletion ConNF/Setup/Litter.lean → ConNF/Base/Litter.lean
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import ConNF.Setup.TypeIndex
import ConNF.Base.TypeIndex

/-!
# Litters
Expand Down
2 changes: 1 addition & 1 deletion ConNF/Setup/NearLitter.lean → ConNF/Base/NearLitter.lean
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import ConNF.Setup.Atom
import ConNF.Base.Atom

/-!
# Near-litters
Expand Down
8 changes: 4 additions & 4 deletions ConNF/Setup/Params.lean → ConNF/Base/Params.lean
View file
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
import Mathlib.Order.Interval.Set.Infinite
import ConNF.Basic.Cardinal
import ConNF.Basic.Ordinal
import ConNF.Basic.Transfer
import ConNF.Basic.WellOrder
import ConNF.Background.Cardinal
import ConNF.Background.Ordinal
import ConNF.Background.Transfer
import ConNF.Background.WellOrder

/-!
# Model parameters
Expand Down
2 changes: 1 addition & 1 deletion ConNF/Setup/Position.lean → ConNF/Base/Position.lean
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import ConNF.Setup.Params
import ConNF.Base.Params

/-!
# Position functions
Expand Down
6 changes: 3 additions & 3 deletions ConNF/Setup/Small.lean → ConNF/Base/Small.lean
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
import ConNF.Basic.Rel
import ConNF.Basic.Set
import ConNF.Setup.Params
import ConNF.Background.Rel
import ConNF.Background.Set
import ConNF.Base.Params

/-!
# Smallness
Expand Down
2 changes: 1 addition & 1 deletion ConNF/Setup/TypeIndex.lean → ConNF/Base/TypeIndex.lean
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import ConNF.Setup.Params
import ConNF.Base.Params

/-!
# Type indices
Expand Down
6 changes: 3 additions & 3 deletions ConNF/Setup/CoherentData.lean → ConNF/Coherent/CoherentData.lean
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
import ConNF.Setup.Fuzz
import ConNF.Setup.Level
import ConNF.Setup.ModelData
import ConNF.Coherent.Fuzz
import ConNF.Levels.Level
import ConNF.Coherent.ModelData

/-!
# Coherent data
Expand Down
4 changes: 2 additions & 2 deletions ConNF/Setup/Enumeration.lean → ConNF/Coherent/Enumeration.lean
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
import ConNF.Basic.Rel
import ConNF.Setup.Small
import ConNF.Background.Rel
import ConNF.Base.Small

/-!
# Enumerations
Expand Down
4 changes: 2 additions & 2 deletions ConNF/Setup/Fuzz.lean → ConNF/Coherent/Fuzz.lean
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
import ConNF.Setup.BasePositions
import ConNF.Setup.ModelData
import ConNF.Levels.BasePositions
import ConNF.Coherent.ModelData

/-!
# The `fuzz` map
Expand Down
4 changes: 2 additions & 2 deletions ConNF/Setup/ModelData.lean → ConNF/Coherent/ModelData.lean
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
import ConNF.Setup.StrSet
import ConNF.Setup.Support
import ConNF.Levels.StrSet
import ConNF.Coherent.Support

/-!
# Model data
Expand Down
4 changes: 2 additions & 2 deletions ConNF/Setup/PathEnumeration.lean → ConNF/Coherent/PathEnumeration.lean
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
import ConNF.Setup.Enumeration
import ConNF.Setup.StrPerm
import ConNF.Coherent.Enumeration
import ConNF.Levels.StrPerm

/-!
# Enumerations over paths
Expand Down
2 changes: 1 addition & 1 deletion ConNF/Setup/Support.lean → ConNF/Coherent/Support.lean
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import ConNF.Setup.PathEnumeration
import ConNF.Coherent.PathEnumeration

/-!
# Supports
Expand Down
2 changes: 1 addition & 1 deletion ConNF/Construction/Code.lean
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import ConNF.Setup.CoherentData
import ConNF.Coherent.CoherentData

/-!
# Codes
Expand Down
2 changes: 1 addition & 1 deletion ConNF/Counting/CodingFunction.lean
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import ConNF.Setup.CoherentData
import ConNF.Coherent.CoherentData

/-!
# Coding functions
Expand Down
2 changes: 1 addition & 1 deletion ConNF/Counting/Twist.lean
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import ConNF.Setup.ModelData
import ConNF.Coherent.ModelData

/-!
# Twisting sets
Expand Down
2 changes: 1 addition & 1 deletion ConNF/FOA/BaseApprox.lean
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import ConNF.Setup.Support
import ConNF.Coherent.Support
import ConNF.FOA.Coherent

/-!
Expand Down
2 changes: 1 addition & 1 deletion ConNF/FOA/Coherent.lean
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import ConNF.Setup.CoherentData
import ConNF.Coherent.CoherentData
import ConNF.FOA.Inflexible

/-!
Expand Down
2 changes: 1 addition & 1 deletion ConNF/FOA/FlexApprox.lean
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import ConNF.Basic.PermutativeExtension
import ConNF.Background.PermutativeExtension
import ConNF.FOA.BaseAction
import ConNF.FOA.StrApprox

Expand Down
2 changes: 1 addition & 1 deletion ConNF/FOA/Inflexible.lean
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import ConNF.Setup.CoherentData
import ConNF.Coherent.CoherentData

/-!
# New file
Expand Down
2 changes: 1 addition & 1 deletion ConNF/FOA/StrApprox.lean
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import ConNF.Setup.CoherentData
import ConNF.Coherent.CoherentData
import ConNF.FOA.BaseApprox

/-!
Expand Down
4 changes: 2 additions & 2 deletions ConNF/Setup/BasePositions.lean → ConNF/Levels/BasePositions.lean
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
import ConNF.Setup.Deny
import ConNF.Setup.NearLitter
import ConNF.Levels.Deny
import ConNF.Base.NearLitter

/-!
# Base positions
Expand Down
2 changes: 1 addition & 1 deletion ConNF/Setup/Deny.lean → ConNF/Levels/Deny.lean
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import ConNF.Setup.Position
import ConNF.Base.Position

/-!
# Injective functions from denied sets
Expand Down
2 changes: 1 addition & 1 deletion ConNF/Setup/Level.lean → ConNF/Levels/Level.lean
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import ConNF.Setup.TypeIndex
import ConNF.Base.TypeIndex

/-!
# Levels
Expand Down
2 changes: 1 addition & 1 deletion ConNF/Setup/Path.lean → ConNF/Levels/Path.lean
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import ConNF.Setup.TypeIndex
import ConNF.Base.TypeIndex

/-!
# Paths of type indices
Expand Down
4 changes: 2 additions & 2 deletions ConNF/Setup/StrPerm.lean → ConNF/Levels/StrPerm.lean
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
import ConNF.Setup.BasePerm
import ConNF.Setup.Tree
import ConNF.Base.BasePerm
import ConNF.Levels.Tree

/-!
# Structural permutations
Expand Down
2 changes: 1 addition & 1 deletion ConNF/Setup/StrSet.lean → ConNF/Levels/StrSet.lean
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import ConNF.Setup.StrPerm
import ConNF.Levels.StrPerm

/-!
# Structural sets
Expand Down
2 changes: 1 addition & 1 deletion ConNF/Setup/Tree.lean → ConNF/Levels/Tree.lean
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import ConNF.Setup.Path
import ConNF.Levels.Path

/-!
# Trees
Expand Down
2 changes: 1 addition & 1 deletion ConNF/Model/InductionStatement.lean
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import ConNF.Setup.CoherentData
import ConNF.Coherent.CoherentData
import ConNF.Construction.Code

/-!
Expand Down
2 changes: 1 addition & 1 deletion ConNF/Model/RunInduction.lean
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import ConNF.Basic.InductiveConstruction
import ConNF.Background.InductiveConstruction
import ConNF.Model.ConstructHypothesis

/-!
Expand Down
2 changes: 1 addition & 1 deletion ConNF/Strong/SpecSame.lean
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
import ConNF.FOA.StrActionFOA
import ConNF.Counting.Strong
import ConNF.Strong.Strong
import ConNF.Strong.Spec

/-!
Expand Down
2 changes: 1 addition & 1 deletion ConNF/Counting/Strong.lean → ConNF/Strong/Strong.lean
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import ConNF.Basic.ReflTransGen
import ConNF.Background.ReflTransGen
import ConNF.FOA.Inflexible

/-!
Expand Down

0 comments on commit 8896e41

Please sign in to comment.