Move old code into Old directory

Signed-off-by: zeramorphic <[email protected]>
leanprover-community · Aug 19, 2024 · cca28dc · cca28dc
1 parent 7b5a322
commit cca28dc
Show file tree

Hide file tree

Showing 115 changed files with 164 additions and 25 deletions.
diff --git a/.gitignore b/.gitignore
@@ -1,4 +1,4 @@
-/build
-/lake-packages/*
-/.lake/*
+build
+lake-packages/*
+**/.lake
 **.olean
diff --git a/ConNF.lean b/ConNF.lean
@@ -1,8 +1 @@
-import ConNF.Mathlib
-import ConNF.BaseType
-import ConNF.Structural
-import ConNF.Fuzz
-import ConNF.Construction
-import ConNF.FOA
-import ConNF.Counting
-import ConNF.Model
+def hello := "world"
diff --git a/Old/ConNF.lean b/Old/ConNF.lean
@@ -0,0 +1,8 @@
+import ConNF.Mathlib
+import ConNF.BaseType
+import ConNF.Structural
+import ConNF.Fuzz
+import ConNF.Construction
+import ConNF.FOA
+import ConNF.Counting
+import ConNF.Model
diff --git a/ConNF/BaseType.lean → Old/ConNF/BaseType.lean b/ConNF/BaseType.lean → Old/ConNF/BaseType.lean
diff --git a/ConNF/BaseType/Atom.lean → Old/ConNF/BaseType/Atom.lean b/ConNF/BaseType/Atom.lean → Old/ConNF/BaseType/Atom.lean
diff --git a/ConNF/BaseType/BasePerm.lean → Old/ConNF/BaseType/BasePerm.lean b/ConNF/BaseType/BasePerm.lean → Old/ConNF/BaseType/BasePerm.lean
diff --git a/ConNF/BaseType/Litter.lean → Old/ConNF/BaseType/Litter.lean b/ConNF/BaseType/Litter.lean → Old/ConNF/BaseType/Litter.lean
diff --git a/ConNF/BaseType/NearLitter.lean → Old/ConNF/BaseType/NearLitter.lean b/ConNF/BaseType/NearLitter.lean → Old/ConNF/BaseType/NearLitter.lean
diff --git a/ConNF/BaseType/Params.lean → Old/ConNF/BaseType/Params.lean b/ConNF/BaseType/Params.lean → Old/ConNF/BaseType/Params.lean
diff --git a/ConNF/BaseType/Small.lean → Old/ConNF/BaseType/Small.lean b/ConNF/BaseType/Small.lean → Old/ConNF/BaseType/Small.lean
diff --git a/ConNF/Construction.lean → Old/ConNF/Construction.lean b/ConNF/Construction.lean → Old/ConNF/Construction.lean
diff --git a/ConNF/Construction/Cloud.lean → Old/ConNF/Construction/Cloud.lean b/ConNF/Construction/Cloud.lean → Old/ConNF/Construction/Cloud.lean
diff --git a/ConNF/Construction/Code.lean → Old/ConNF/Construction/Code.lean b/ConNF/Construction/Code.lean → Old/ConNF/Construction/Code.lean
diff --git a/ConNF/Construction/CodeEquiv.lean → Old/ConNF/Construction/CodeEquiv.lean b/ConNF/Construction/CodeEquiv.lean → Old/ConNF/Construction/CodeEquiv.lean
diff --git a/ConNF/Construction/Hypotheses.lean → Old/ConNF/Construction/Hypotheses.lean b/ConNF/Construction/Hypotheses.lean → Old/ConNF/Construction/Hypotheses.lean
diff --git a/ConNF/Construction/NewAllowable.lean → Old/ConNF/Construction/NewAllowable.lean b/ConNF/Construction/NewAllowable.lean → Old/ConNF/Construction/NewAllowable.lean
diff --git a/ConNF/Construction/NewTSet.lean → Old/ConNF/Construction/NewTSet.lean b/ConNF/Construction/NewTSet.lean → Old/ConNF/Construction/NewTSet.lean
diff --git a/ConNF/Construction/Position.lean → Old/ConNF/Construction/Position.lean b/ConNF/Construction/Position.lean → Old/ConNF/Construction/Position.lean
diff --git a/ConNF/Counting.lean → Old/ConNF/Counting.lean b/ConNF/Counting.lean → Old/ConNF/Counting.lean
diff --git a/ConNF/Counting/CodingFunction.lean → Old/ConNF/Counting/CodingFunction.lean b/ConNF/Counting/CodingFunction.lean → Old/ConNF/Counting/CodingFunction.lean
diff --git a/ConNF/Counting/Conclusions.lean → Old/ConNF/Counting/Conclusions.lean b/ConNF/Counting/Conclusions.lean → Old/ConNF/Counting/Conclusions.lean
diff --git a/ConNF/Counting/CountCodingFunction.lean → Old/ConNF/Counting/CountCodingFunction.lean b/ConNF/Counting/CountCodingFunction.lean → Old/ConNF/Counting/CountCodingFunction.lean
diff --git a/ConNF/Counting/CountRaisedSingleton.lean → Old/ConNF/Counting/CountRaisedSingleton.lean b/ConNF/Counting/CountRaisedSingleton.lean → Old/ConNF/Counting/CountRaisedSingleton.lean
diff --git a/ConNF/Counting/CountSpec.lean → Old/ConNF/Counting/CountSpec.lean b/ConNF/Counting/CountSpec.lean → Old/ConNF/Counting/CountSpec.lean
diff --git a/ConNF/Counting/CountSupportOrbit.lean → Old/ConNF/Counting/CountSupportOrbit.lean b/ConNF/Counting/CountSupportOrbit.lean → Old/ConNF/Counting/CountSupportOrbit.lean
diff --git a/ConNF/Counting/ExistsSpec.lean → Old/ConNF/Counting/ExistsSpec.lean b/ConNF/Counting/ExistsSpec.lean → Old/ConNF/Counting/ExistsSpec.lean
diff --git a/ConNF/Counting/Hypotheses.lean → Old/ConNF/Counting/Hypotheses.lean b/ConNF/Counting/Hypotheses.lean → Old/ConNF/Counting/Hypotheses.lean
diff --git a/ConNF/Counting/Recode.lean → Old/ConNF/Counting/Recode.lean b/ConNF/Counting/Recode.lean → Old/ConNF/Counting/Recode.lean
diff --git a/ConNF/Counting/Spec.lean → Old/ConNF/Counting/Spec.lean b/ConNF/Counting/Spec.lean → Old/ConNF/Counting/Spec.lean
diff --git a/ConNF/Counting/SpecSMul.lean → Old/ConNF/Counting/SpecSMul.lean b/ConNF/Counting/SpecSMul.lean → Old/ConNF/Counting/SpecSMul.lean
diff --git a/ConNF/Counting/SpecSame.lean → Old/ConNF/Counting/SpecSame.lean b/ConNF/Counting/SpecSame.lean → Old/ConNF/Counting/SpecSame.lean
diff --git a/ConNF/Counting/StrongSupport.lean → Old/ConNF/Counting/StrongSupport.lean b/ConNF/Counting/StrongSupport.lean → Old/ConNF/Counting/StrongSupport.lean
diff --git a/ConNF/Counting/SupportOrbit.lean → Old/ConNF/Counting/SupportOrbit.lean b/ConNF/Counting/SupportOrbit.lean → Old/ConNF/Counting/SupportOrbit.lean
diff --git a/ConNF/Counting/Twist.lean → Old/ConNF/Counting/Twist.lean b/ConNF/Counting/Twist.lean → Old/ConNF/Counting/Twist.lean
diff --git a/ConNF/FOA.lean → Old/ConNF/FOA.lean b/ConNF/FOA.lean → Old/ConNF/FOA.lean
diff --git a/ConNF/FOA/Approx.lean → Old/ConNF/FOA/Approx.lean b/ConNF/FOA/Approx.lean → Old/ConNF/FOA/Approx.lean
diff --git a/ConNF/FOA/Approx/BaseApprox.lean → Old/ConNF/FOA/Approx/BaseApprox.lean b/ConNF/FOA/Approx/BaseApprox.lean → Old/ConNF/FOA/Approx/BaseApprox.lean
diff --git a/ConNF/FOA/Approx/StructApprox.lean → Old/ConNF/FOA/Approx/StructApprox.lean b/ConNF/FOA/Approx/StructApprox.lean → Old/ConNF/FOA/Approx/StructApprox.lean
diff --git a/ConNF/FOA/Basic.lean → Old/ConNF/FOA/Basic.lean b/ConNF/FOA/Basic.lean → Old/ConNF/FOA/Basic.lean
diff --git a/ConNF/FOA/Basic/CompleteOrbit.lean → Old/ConNF/FOA/Basic/CompleteOrbit.lean b/ConNF/FOA/Basic/CompleteOrbit.lean → Old/ConNF/FOA/Basic/CompleteOrbit.lean
diff --git a/ConNF/FOA/Basic/Constrains.lean → Old/ConNF/FOA/Basic/Constrains.lean b/ConNF/FOA/Basic/Constrains.lean → Old/ConNF/FOA/Basic/Constrains.lean
diff --git a/ConNF/FOA/Basic/Flexible.lean → Old/ConNF/FOA/Basic/Flexible.lean b/ConNF/FOA/Basic/Flexible.lean → Old/ConNF/FOA/Basic/Flexible.lean
diff --git a/ConNF/FOA/Basic/Hypotheses.lean → Old/ConNF/FOA/Basic/Hypotheses.lean b/ConNF/FOA/Basic/Hypotheses.lean → Old/ConNF/FOA/Basic/Hypotheses.lean
diff --git a/ConNF/FOA/Basic/Sublitter.lean → Old/ConNF/FOA/Basic/Sublitter.lean b/ConNF/FOA/Basic/Sublitter.lean → Old/ConNF/FOA/Basic/Sublitter.lean
diff --git a/ConNF/FOA/Complete.lean → Old/ConNF/FOA/Complete.lean b/ConNF/FOA/Complete.lean → Old/ConNF/FOA/Complete.lean
diff --git a/ConNF/FOA/Complete/AtomCompletion.lean → Old/ConNF/FOA/Complete/AtomCompletion.lean b/ConNF/FOA/Complete/AtomCompletion.lean → Old/ConNF/FOA/Complete/AtomCompletion.lean
diff --git a/ConNF/FOA/Complete/CompleteAction.lean → Old/ConNF/FOA/Complete/CompleteAction.lean b/ConNF/FOA/Complete/CompleteAction.lean → Old/ConNF/FOA/Complete/CompleteAction.lean
diff --git a/ConNF/FOA/Complete/FlexibleCompletion.lean → ...onNF/FOA/Complete/FlexibleCompletion.lean b/ConNF/FOA/Complete/FlexibleCompletion.lean → ...onNF/FOA/Complete/FlexibleCompletion.lean
diff --git a/ConNF/FOA/Complete/HypAction.lean → Old/ConNF/FOA/Complete/HypAction.lean b/ConNF/FOA/Complete/HypAction.lean → Old/ConNF/FOA/Complete/HypAction.lean
diff --git a/ConNF/FOA/Complete/LitterCompletion.lean → Old/ConNF/FOA/Complete/LitterCompletion.lean b/ConNF/FOA/Complete/LitterCompletion.lean → Old/ConNF/FOA/Complete/LitterCompletion.lean
diff --git a/ConNF/FOA/Complete/NearLitterCompletion.lean → ...NF/FOA/Complete/NearLitterCompletion.lean b/ConNF/FOA/Complete/NearLitterCompletion.lean → ...NF/FOA/Complete/NearLitterCompletion.lean
diff --git a/ConNF/FOA/Corollaries.lean → Old/ConNF/FOA/Corollaries.lean b/ConNF/FOA/Corollaries.lean → Old/ConNF/FOA/Corollaries.lean
diff --git a/ConNF/FOA/LAction.lean → Old/ConNF/FOA/LAction.lean b/ConNF/FOA/LAction.lean → Old/ConNF/FOA/LAction.lean
diff --git a/ConNF/FOA/LAction/BaseLAction.lean → Old/ConNF/FOA/LAction/BaseLAction.lean b/ConNF/FOA/LAction/BaseLAction.lean → Old/ConNF/FOA/LAction/BaseLAction.lean
diff --git a/ConNF/FOA/LAction/Complete.lean → Old/ConNF/FOA/LAction/Complete.lean b/ConNF/FOA/LAction/Complete.lean → Old/ConNF/FOA/LAction/Complete.lean
diff --git a/ConNF/FOA/LAction/FillAtomOrbits.lean → Old/ConNF/FOA/LAction/FillAtomOrbits.lean b/ConNF/FOA/LAction/FillAtomOrbits.lean → Old/ConNF/FOA/LAction/FillAtomOrbits.lean
diff --git a/ConNF/FOA/LAction/FillAtomRange.lean → Old/ConNF/FOA/LAction/FillAtomRange.lean b/ConNF/FOA/LAction/FillAtomRange.lean → Old/ConNF/FOA/LAction/FillAtomRange.lean
diff --git a/ConNF/FOA/LAction/StructLAction.lean → Old/ConNF/FOA/LAction/StructLAction.lean b/ConNF/FOA/LAction/StructLAction.lean → Old/ConNF/FOA/LAction/StructLAction.lean
diff --git a/ConNF/FOA/LAction/ToApprox.lean → Old/ConNF/FOA/LAction/ToApprox.lean b/ConNF/FOA/LAction/ToApprox.lean → Old/ConNF/FOA/LAction/ToApprox.lean
diff --git a/ConNF/FOA/NLAction.lean → Old/ConNF/FOA/NLAction.lean b/ConNF/FOA/NLAction.lean → Old/ConNF/FOA/NLAction.lean
diff --git a/ConNF/FOA/NLAction/BaseNLAction.lean → Old/ConNF/FOA/NLAction/BaseNLAction.lean b/ConNF/FOA/NLAction/BaseNLAction.lean → Old/ConNF/FOA/NLAction/BaseNLAction.lean
diff --git a/ConNF/FOA/NLAction/StructNLAction.lean → Old/ConNF/FOA/NLAction/StructNLAction.lean b/ConNF/FOA/NLAction/StructNLAction.lean → Old/ConNF/FOA/NLAction/StructNLAction.lean
diff --git a/ConNF/FOA/Properties.lean → Old/ConNF/FOA/Properties.lean b/ConNF/FOA/Properties.lean → Old/ConNF/FOA/Properties.lean
diff --git a/ConNF/FOA/Properties/Bijective.lean → Old/ConNF/FOA/Properties/Bijective.lean b/ConNF/FOA/Properties/Bijective.lean → Old/ConNF/FOA/Properties/Bijective.lean
diff --git a/ConNF/FOA/Properties/ConstrainedAction.lean → ...nNF/FOA/Properties/ConstrainedAction.lean b/ConNF/FOA/Properties/ConstrainedAction.lean → ...nNF/FOA/Properties/ConstrainedAction.lean
diff --git a/ConNF/FOA/Properties/Injective.lean → Old/ConNF/FOA/Properties/Injective.lean b/ConNF/FOA/Properties/Injective.lean → Old/ConNF/FOA/Properties/Injective.lean
diff --git a/ConNF/FOA/Properties/Surjective.lean → Old/ConNF/FOA/Properties/Surjective.lean b/ConNF/FOA/Properties/Surjective.lean → Old/ConNF/FOA/Properties/Surjective.lean
diff --git a/ConNF/FOA/Result.lean → Old/ConNF/FOA/Result.lean b/ConNF/FOA/Result.lean → Old/ConNF/FOA/Result.lean
diff --git a/ConNF/Fuzz.lean → Old/ConNF/Fuzz.lean b/ConNF/Fuzz.lean → Old/ConNF/Fuzz.lean
diff --git a/ConNF/Fuzz/Construction.lean → Old/ConNF/Fuzz/Construction.lean b/ConNF/Fuzz/Construction.lean → Old/ConNF/Fuzz/Construction.lean
diff --git a/ConNF/Fuzz/Hypotheses.lean → Old/ConNF/Fuzz/Hypotheses.lean b/ConNF/Fuzz/Hypotheses.lean → Old/ConNF/Fuzz/Hypotheses.lean
diff --git a/ConNF/Fuzz/Position.lean → Old/ConNF/Fuzz/Position.lean b/ConNF/Fuzz/Position.lean → Old/ConNF/Fuzz/Position.lean
diff --git a/ConNF/Mathlib.lean → Old/ConNF/Mathlib.lean b/ConNF/Mathlib.lean → Old/ConNF/Mathlib.lean
diff --git a/ConNF/Mathlib/Cardinal.lean → Old/ConNF/Mathlib/Cardinal.lean b/ConNF/Mathlib/Cardinal.lean → Old/ConNF/Mathlib/Cardinal.lean
diff --git a/ConNF/Mathlib/Equiv.lean → Old/ConNF/Mathlib/Equiv.lean b/ConNF/Mathlib/Equiv.lean → Old/ConNF/Mathlib/Equiv.lean
diff --git a/ConNF/Mathlib/Group.lean → Old/ConNF/Mathlib/Group.lean b/ConNF/Mathlib/Group.lean → Old/ConNF/Mathlib/Group.lean
diff --git a/ConNF/Mathlib/GroupAction.lean → Old/ConNF/Mathlib/GroupAction.lean b/ConNF/Mathlib/GroupAction.lean → Old/ConNF/Mathlib/GroupAction.lean
diff --git a/ConNF/Mathlib/Logic.lean → Old/ConNF/Mathlib/Logic.lean b/ConNF/Mathlib/Logic.lean → Old/ConNF/Mathlib/Logic.lean
diff --git a/ConNF/Mathlib/Logic/Equiv/PartialPerm.lean → ...onNF/Mathlib/Logic/Equiv/PartialPerm.lean b/ConNF/Mathlib/Logic/Equiv/PartialPerm.lean → ...onNF/Mathlib/Logic/Equiv/PartialPerm.lean
diff --git a/ConNF/Mathlib/Nat.lean → Old/ConNF/Mathlib/Nat.lean b/ConNF/Mathlib/Nat.lean → Old/ConNF/Mathlib/Nat.lean
diff --git a/ConNF/Mathlib/Order.lean → Old/ConNF/Mathlib/Order.lean b/ConNF/Mathlib/Order.lean → Old/ConNF/Mathlib/Order.lean
diff --git a/ConNF/Mathlib/Ordinal.lean → Old/ConNF/Mathlib/Ordinal.lean b/ConNF/Mathlib/Ordinal.lean → Old/ConNF/Mathlib/Ordinal.lean
diff --git a/ConNF/Mathlib/PFun.lean → Old/ConNF/Mathlib/PFun.lean b/ConNF/Mathlib/PFun.lean → Old/ConNF/Mathlib/PFun.lean
diff --git a/ConNF/Mathlib/Pointwise.lean → Old/ConNF/Mathlib/Pointwise.lean b/ConNF/Mathlib/Pointwise.lean → Old/ConNF/Mathlib/Pointwise.lean
diff --git a/ConNF/Mathlib/Support.lean → Old/ConNF/Mathlib/Support.lean b/ConNF/Mathlib/Support.lean → Old/ConNF/Mathlib/Support.lean
diff --git a/ConNF/Mathlib/Transfer.lean → Old/ConNF/Mathlib/Transfer.lean b/ConNF/Mathlib/Transfer.lean → Old/ConNF/Mathlib/Transfer.lean
diff --git a/ConNF/Mathlib/WithBot.lean → Old/ConNF/Mathlib/WithBot.lean b/ConNF/Mathlib/WithBot.lean → Old/ConNF/Mathlib/WithBot.lean
diff --git a/ConNF/Model.lean → Old/ConNF/Model.lean b/ConNF/Model.lean → Old/ConNF/Model.lean
diff --git a/ConNF/Model/BasePositions.lean → Old/ConNF/Model/BasePositions.lean b/ConNF/Model/BasePositions.lean → Old/ConNF/Model/BasePositions.lean
diff --git a/ConNF/Model/Basic.lean → Old/ConNF/Model/Basic.lean b/ConNF/Model/Basic.lean → Old/ConNF/Model/Basic.lean
diff --git a/ConNF/Model/CountZero.lean → Old/ConNF/Model/CountZero.lean b/ConNF/Model/CountZero.lean → Old/ConNF/Model/CountZero.lean
diff --git a/ConNF/Model/FOA.lean → Old/ConNF/Model/FOA.lean b/ConNF/Model/FOA.lean → Old/ConNF/Model/FOA.lean
diff --git a/ConNF/Model/MainInduction.lean → Old/ConNF/Model/MainInduction.lean b/ConNF/Model/MainInduction.lean → Old/ConNF/Model/MainInduction.lean
diff --git a/ConNF/Model/Predicative.lean → Old/ConNF/Model/Predicative.lean b/ConNF/Model/Predicative.lean → Old/ConNF/Model/Predicative.lean
diff --git a/ConNF/Model/RaiseStrong.lean → Old/ConNF/Model/RaiseStrong.lean b/ConNF/Model/RaiseStrong.lean → Old/ConNF/Model/RaiseStrong.lean
diff --git a/ConNF/Model/Redefinitions.lean → Old/ConNF/Model/Redefinitions.lean b/ConNF/Model/Redefinitions.lean → Old/ConNF/Model/Redefinitions.lean
diff --git a/ConNF/Model/Result.lean → Old/ConNF/Model/Result.lean b/ConNF/Model/Result.lean → Old/ConNF/Model/Result.lean
diff --git a/ConNF/Model/Union.lean → Old/ConNF/Model/Union.lean b/ConNF/Model/Union.lean → Old/ConNF/Model/Union.lean
diff --git a/ConNF/New/DerivativeTest.lean → Old/ConNF/New/DerivativeTest.lean b/ConNF/New/DerivativeTest.lean → Old/ConNF/New/DerivativeTest.lean
diff --git a/ConNF/New/RelationTest.lean → Old/ConNF/New/RelationTest.lean b/ConNF/New/RelationTest.lean → Old/ConNF/New/RelationTest.lean
diff --git a/ConNF/Structural.lean → Old/ConNF/Structural.lean b/ConNF/Structural.lean → Old/ConNF/Structural.lean
diff --git a/ConNF/Structural/Enumeration.lean → Old/ConNF/Structural/Enumeration.lean b/ConNF/Structural/Enumeration.lean → Old/ConNF/Structural/Enumeration.lean
diff --git a/ConNF/Structural/Index.lean → Old/ConNF/Structural/Index.lean b/ConNF/Structural/Index.lean → Old/ConNF/Structural/Index.lean
diff --git a/ConNF/Structural/StructPerm.lean → Old/ConNF/Structural/StructPerm.lean b/ConNF/Structural/StructPerm.lean → Old/ConNF/Structural/StructPerm.lean
diff --git a/ConNF/Structural/StructSet.lean → Old/ConNF/Structural/StructSet.lean b/ConNF/Structural/StructSet.lean → Old/ConNF/Structural/StructSet.lean
diff --git a/ConNF/Structural/Support.lean → Old/ConNF/Structural/Support.lean b/ConNF/Structural/Support.lean → Old/ConNF/Structural/Support.lean
diff --git a/ConNF/Structural/Tree.lean → Old/ConNF/Structural/Tree.lean b/ConNF/Structural/Tree.lean → Old/ConNF/Structural/Tree.lean
diff --git a/Naming.md → Old/Naming.md b/Naming.md → Old/Naming.md
diff --git a/TODO.md → Old/TODO.md b/TODO.md → Old/TODO.md
diff --git a/Old/lake-manifest.json b/Old/lake-manifest.json
@@ -0,0 +1,115 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "c0efc1fd2a0bec51bd55c5b17348af13d7419239",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "622d52c803db99ff4ea4fb442c1db9e91aed944c",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "d1b33202c3a29a079f292de65ea438648123b635",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.39",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/mathlib4.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "bd8361bbeb9dc7de717cede1d6f3dd6eefe9722c",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/acmepjz/md4lean",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "9148a0a7506099963925cf239c491fcda5ed0044",
+   "name": "MD4Lean",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "f93115d0209de6db335725dee900d379f40c0317",
+   "name": "UnicodeBasic",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/dupuisf/BibtexQuery",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "bd8747df9ee72fca365efa5bd3bd0d8dcd083b9f",
+   "name": "BibtexQuery",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/doc-gen4",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "b941c425f6f0f1dc45fe13b850ffa7db1bb20d04",
+   "name": "«doc-gen4»",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "ConNF",
+ "lakeDir": ".lake"}
diff --git a/Old/lakefile.toml b/Old/lakefile.toml
@@ -0,0 +1,22 @@
+name = "ConNF"
+defaultTargets = ["ConNF"]
+
+[moreServerOptions]
+autoImplicit = false
+relaxedAutoImplicit = false
+pp.proofs.withType = false
+
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4.git"
+
+[[require]]
+name = "doc-gen4"
+git = "https://github.com/leanprover/doc-gen4"
+rev = "main"
+
+[[lean_lib]]
+name = "ConNF"
+
+[[lean_lib]]
+name = "DependencyGraph"
diff --git a/Old/lean-toolchain b/Old/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.10.0-rc2
diff --git a/blueprint/src/chapters/model.tex b/blueprint/src/chapters/model.tex
@@ -65,7 +65,7 @@ \section{Raising strong supports}
   Then by coinjectivity we can apply the above result, giving that either there is \( B \) such that \( A = B^\alpha \) and \( \rho_B(a_1) = a_2 \), or there is no such \( B \), and \( a_1 = a_2 \).
   In either case, the result is easy to show.
 
-  The result for litters follows from the fact that the condition on \( U \) implies that proofs of inflexiblity of litters in \( U \) correspond bijectively to proofs of inflexibility of litters in \( U^\alpha \).
+  The result for litters follows from the fact that the condition on \( U \) implies that proofs of inflexiblity of litters in \( U \) correspond bijectively to proofs of inflexibility of litters in \( U^\alpha \).\footnote{TODO: Probably want more details when we get here.}
 \end{proof}
 \begin{proposition}
   \uses{def:Strong}

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c0efc1fd2a0bec51bd55c5b17348af13d7419239",
+   "rev": "a975dea2c4d8258a55b4f9861c537e2bb0f9ef63",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
+   "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "622d52c803db99ff4ea4fb442c1db9e91aed944c",
+   "rev": "776a5a8f9c789395796e442d78a9d4cb9c4c9d03",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,27 +35,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d1b33202c3a29a079f292de65ea438648123b635",
+   "rev": "a96aee5245720f588876021b6a0aa73efee49c76",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.39",
+   "inputRev": "v0.0.41",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
+   "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "bd8361bbeb9dc7de717cede1d6f3dd6eefe9722c",
+   "rev": "b3ae244300f97308f07d01ba948d345f354a1001",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9148a0a7506099963925cf239c491fcda5ed0044",
+   "rev": "5e95f4776be5e048364f325c7e9d619bb56fb005",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f93115d0209de6db335725dee900d379f40c0317",
+   "rev": "5c11428272fe190b7e726ebe448f93437d057b74",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -105,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b941c425f6f0f1dc45fe13b850ffa7db1bb20d04",
+   "rev": "cc93eea2cd48f119cc94027623b1f89055b468f1",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.10.0-rc2
+leanprover/lean4:v4.11.0-rc2
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.10.0-rc2
		leanprover/lean4:v4.11.0-rc2