diff --git a/Foundation.lean b/Foundation.lean index 1e85d6968..0bccdd137 100644 --- a/Foundation.lean +++ b/Foundation.lean @@ -1,22 +1,18 @@ module -- shake: keep-all --deprecated_module: ignore -public import Foundation.FirstOrder.Arithmetic.Basic public import Foundation.FirstOrder.Arithmetic.Basic.Hierarchy public import Foundation.FirstOrder.Arithmetic.Basic.Misc public import Foundation.FirstOrder.Arithmetic.Basic.Model public import Foundation.FirstOrder.Arithmetic.Basic.Monotone -public import Foundation.FirstOrder.Arithmetic.Definability public import Foundation.FirstOrder.Arithmetic.Definability.Absoluteness public import Foundation.FirstOrder.Arithmetic.Definability.BoundedDefinable public import Foundation.FirstOrder.Arithmetic.Definability.Definable public import Foundation.FirstOrder.Arithmetic.Definability.Hierarchy -public import Foundation.FirstOrder.Arithmetic.Exponential public import Foundation.FirstOrder.Arithmetic.Exponential.Bit public import Foundation.FirstOrder.Arithmetic.Exponential.Exp public import Foundation.FirstOrder.Arithmetic.Exponential.Log public import Foundation.FirstOrder.Arithmetic.Exponential.PPow2 public import Foundation.FirstOrder.Arithmetic.Exponential.Pow2 -public import Foundation.FirstOrder.Arithmetic.HFS public import Foundation.FirstOrder.Arithmetic.HFS.Basic public import Foundation.FirstOrder.Arithmetic.HFS.Coding public import Foundation.FirstOrder.Arithmetic.HFS.Fixpoint @@ -36,7 +32,6 @@ public import Foundation.FirstOrder.Arithmetic.R0.Representation public import Foundation.FirstOrder.Arithmetic.Schemata public import Foundation.FirstOrder.Arithmetic.TA.Basic public import Foundation.FirstOrder.Arithmetic.TA.Nonstandard -public import Foundation.FirstOrder.Basic public import Foundation.FirstOrder.Basic.AesopInit public import Foundation.FirstOrder.Basic.BinderNotation public import Foundation.FirstOrder.Basic.Calculus @@ -59,7 +54,6 @@ public import Foundation.FirstOrder.Bootstrapping.DerivabilityCondition.D3 public import Foundation.FirstOrder.Bootstrapping.DerivabilityCondition.EquationalTheory public import Foundation.FirstOrder.Bootstrapping.DerivabilityCondition.PeanoMinus public import Foundation.FirstOrder.Bootstrapping.FixedPoint -public import Foundation.FirstOrder.Bootstrapping.Syntax public import Foundation.FirstOrder.Bootstrapping.Syntax.Formula.Basic public import Foundation.FirstOrder.Bootstrapping.Syntax.Formula.Coding public import Foundation.FirstOrder.Bootstrapping.Syntax.Formula.Functions @@ -74,7 +68,6 @@ public import Foundation.FirstOrder.Bootstrapping.Syntax.Term.Coding public import Foundation.FirstOrder.Bootstrapping.Syntax.Term.Functions public import Foundation.FirstOrder.Bootstrapping.Syntax.Term.Typed public import Foundation.FirstOrder.Bootstrapping.Syntax.Theory -public import Foundation.FirstOrder.Completeness public import Foundation.FirstOrder.Completeness.CanonicalModel public import Foundation.FirstOrder.Completeness.CountableSublanguage public import Foundation.FirstOrder.Completeness.CounterModel @@ -108,7 +101,6 @@ public import Foundation.FirstOrder.Kripke.WeakForcing public import Foundation.FirstOrder.NegationTranslation.GoedelGentzen public import Foundation.FirstOrder.Order.Le public import Foundation.FirstOrder.Polarity -public import Foundation.FirstOrder.SetTheory.Basic public import Foundation.FirstOrder.SetTheory.Basic.Axioms public import Foundation.FirstOrder.SetTheory.Basic.Misc public import Foundation.FirstOrder.SetTheory.Basic.Model diff --git a/Foundation/FirstOrder/Arithmetic/Basic.lean b/Foundation/FirstOrder/Arithmetic/Basic.lean deleted file mode 100644 index 7a015eb35..000000000 --- a/Foundation/FirstOrder/Arithmetic/Basic.lean +++ /dev/null @@ -1,6 +0,0 @@ -module - -public import Foundation.FirstOrder.Arithmetic.Basic.Misc -public import Foundation.FirstOrder.Arithmetic.Basic.Monotone -public import Foundation.FirstOrder.Arithmetic.Basic.Hierarchy -public import Foundation.FirstOrder.Arithmetic.Basic.Model \ No newline at end of file diff --git a/Foundation/FirstOrder/Arithmetic/Definability.lean b/Foundation/FirstOrder/Arithmetic/Definability.lean deleted file mode 100644 index ada2904f7..000000000 --- a/Foundation/FirstOrder/Arithmetic/Definability.lean +++ /dev/null @@ -1,6 +0,0 @@ -module - -public import Foundation.FirstOrder.Arithmetic.Definability.Hierarchy -public import Foundation.FirstOrder.Arithmetic.Definability.Definable -public import Foundation.FirstOrder.Arithmetic.Definability.BoundedDefinable -public import Foundation.FirstOrder.Arithmetic.Definability.Absoluteness \ No newline at end of file diff --git a/Foundation/FirstOrder/Arithmetic/Exponential.lean b/Foundation/FirstOrder/Arithmetic/Exponential.lean deleted file mode 100644 index 54ab5f1f2..000000000 --- a/Foundation/FirstOrder/Arithmetic/Exponential.lean +++ /dev/null @@ -1,7 +0,0 @@ -module - -public import Foundation.FirstOrder.Arithmetic.Exponential.Pow2 -public import Foundation.FirstOrder.Arithmetic.Exponential.PPow2 -public import Foundation.FirstOrder.Arithmetic.Exponential.Exp -public import Foundation.FirstOrder.Arithmetic.Exponential.Log -public import Foundation.FirstOrder.Arithmetic.Exponential.Bit \ No newline at end of file diff --git a/Foundation/FirstOrder/Arithmetic/Exponential/Exp.lean b/Foundation/FirstOrder/Arithmetic/Exponential/Exp.lean index 4fc81064c..2a29f1fcd 100644 --- a/Foundation/FirstOrder/Arithmetic/Exponential/Exp.lean +++ b/Foundation/FirstOrder/Arithmetic/Exponential/Exp.lean @@ -1,7 +1,6 @@ module public import Foundation.FirstOrder.Arithmetic.Exponential.PPow2 -public import Mathlib.Algebra.Order.Ring.Basic @[expose] public section /-! diff --git a/Foundation/FirstOrder/Arithmetic/HFS.lean b/Foundation/FirstOrder/Arithmetic/HFS.lean deleted file mode 100644 index f0db95dd2..000000000 --- a/Foundation/FirstOrder/Arithmetic/HFS.lean +++ /dev/null @@ -1,8 +0,0 @@ -module - -public import Foundation.FirstOrder.Arithmetic.HFS.Basic -public import Foundation.FirstOrder.Arithmetic.HFS.Seq -public import Foundation.FirstOrder.Arithmetic.HFS.PRF -public import Foundation.FirstOrder.Arithmetic.HFS.Fixpoint -public import Foundation.FirstOrder.Arithmetic.HFS.Vec -public import Foundation.FirstOrder.Arithmetic.HFS.Coding \ No newline at end of file diff --git a/Foundation/FirstOrder/Arithmetic/HFS/Basic.lean b/Foundation/FirstOrder/Arithmetic/HFS/Basic.lean index a29ef2fcf..ba5cfe8c0 100644 --- a/Foundation/FirstOrder/Arithmetic/HFS/Basic.lean +++ b/Foundation/FirstOrder/Arithmetic/HFS/Basic.lean @@ -1,6 +1,6 @@ module -public import Foundation.FirstOrder.Arithmetic.Exponential +public import Foundation.FirstOrder.Arithmetic.Exponential.Bit @[expose] public section /-! diff --git a/Foundation/FirstOrder/Arithmetic/Induction.lean b/Foundation/FirstOrder/Arithmetic/Induction.lean index 2608035c0..b7ee07c07 100644 --- a/Foundation/FirstOrder/Arithmetic/Induction.lean +++ b/Foundation/FirstOrder/Arithmetic/Induction.lean @@ -1,6 +1,6 @@ module -public import Foundation.FirstOrder.Arithmetic.HFS +public import Foundation.FirstOrder.Arithmetic.HFS.Coding @[expose] public section /-! diff --git a/Foundation/FirstOrder/Arithmetic/Omega1/Basic.lean b/Foundation/FirstOrder/Arithmetic/Omega1/Basic.lean index 71af62bf2..9d5c5a397 100644 --- a/Foundation/FirstOrder/Arithmetic/Omega1/Basic.lean +++ b/Foundation/FirstOrder/Arithmetic/Omega1/Basic.lean @@ -1,6 +1,6 @@ module -public import Foundation.FirstOrder.Arithmetic.Exponential +public import Foundation.FirstOrder.Arithmetic.Exponential.Bit @[expose] public section /-! diff --git a/Foundation/FirstOrder/Arithmetic/PeanoMinus/Functions.lean b/Foundation/FirstOrder/Arithmetic/PeanoMinus/Functions.lean index bb6ac9e18..1c8725d25 100644 --- a/Foundation/FirstOrder/Arithmetic/PeanoMinus/Functions.lean +++ b/Foundation/FirstOrder/Arithmetic/PeanoMinus/Functions.lean @@ -1,6 +1,6 @@ module -public import Foundation.FirstOrder.Arithmetic.Definability +public import Foundation.FirstOrder.Arithmetic.Definability.Absoluteness public import Mathlib.Algebra.Prime.Lemmas public import Foundation.Vorspiel.ExistsUnique diff --git a/Foundation/FirstOrder/Arithmetic/R0/Basic.lean b/Foundation/FirstOrder/Arithmetic/R0/Basic.lean index c64d3f408..01efc8216 100644 --- a/Foundation/FirstOrder/Arithmetic/R0/Basic.lean +++ b/Foundation/FirstOrder/Arithmetic/R0/Basic.lean @@ -1,6 +1,7 @@ module -public import Foundation.FirstOrder.Arithmetic.Basic +public import Foundation.FirstOrder.Arithmetic.Basic.Monotone +public import Foundation.FirstOrder.Arithmetic.Basic.Hierarchy @[expose] public section /-! diff --git a/Foundation/FirstOrder/Arithmetic/TA/Basic.lean b/Foundation/FirstOrder/Arithmetic/TA/Basic.lean index 52b63dc24..a8ddb8878 100644 --- a/Foundation/FirstOrder/Arithmetic/TA/Basic.lean +++ b/Foundation/FirstOrder/Arithmetic/TA/Basic.lean @@ -1,6 +1,7 @@ module -public import Foundation.FirstOrder.Arithmetic.Basic +public import Foundation.FirstOrder.Arithmetic.Basic.Monotone +public import Foundation.FirstOrder.Arithmetic.Basic.Hierarchy @[expose] public section namespace LO.FirstOrder.Arithmetic diff --git a/Foundation/FirstOrder/Basic.lean b/Foundation/FirstOrder/Basic.lean deleted file mode 100644 index f3d9b7952..000000000 --- a/Foundation/FirstOrder/Basic.lean +++ /dev/null @@ -1,17 +0,0 @@ -module - -public import Foundation.FirstOrder.Basic.Syntax.Formula -public import Foundation.FirstOrder.Basic.Syntax.Rew -public import Foundation.FirstOrder.Basic.Semantics.Semantics -public import Foundation.FirstOrder.Basic.Semantics.Elementary -public import Foundation.FirstOrder.Basic.Operator -public import Foundation.FirstOrder.Basic.BinderNotation -public import Foundation.FirstOrder.Basic.Model -public import Foundation.FirstOrder.Basic.Calculus -public import Foundation.FirstOrder.Basic.CutFree -public import Foundation.FirstOrder.Basic.Calculus2 -public import Foundation.FirstOrder.Basic.Coding -public import Foundation.FirstOrder.Basic.Eq -public import Foundation.FirstOrder.Basic.Soundness -public import Foundation.FirstOrder.Basic.Padding -public import Foundation.FirstOrder.Basic.Definability diff --git a/Foundation/FirstOrder/Basic/Calculus.lean b/Foundation/FirstOrder/Basic/Calculus.lean index 143105fa2..aa63c3047 100644 --- a/Foundation/FirstOrder/Basic/Calculus.lean +++ b/Foundation/FirstOrder/Basic/Calculus.lean @@ -2,7 +2,6 @@ module /- public import Foundation.Logic.Calculus -/ public import Foundation.Logic.Calculus -public import Foundation.Propositional.Entailment.AxiomEFQ public import Foundation.FirstOrder.Basic.Syntax.Rew public import Mathlib.Data.List.MinMax diff --git a/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D1.lean b/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D1.lean index 32c52217d..cb149383f 100644 --- a/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D1.lean +++ b/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D1.lean @@ -1,6 +1,6 @@ module -public import Foundation.FirstOrder.Bootstrapping.Syntax +public import Foundation.FirstOrder.Bootstrapping.Syntax.Proof.Coding @[expose] public section /-! diff --git a/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D2.lean b/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D2.lean index e817e9692..40e881867 100644 --- a/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D2.lean +++ b/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D2.lean @@ -1,6 +1,6 @@ module -public import Foundation.FirstOrder.Bootstrapping.Syntax +public import Foundation.FirstOrder.Bootstrapping.Syntax.Proof.Coding @[expose] public section /-! diff --git a/Foundation/FirstOrder/Bootstrapping/FixedPoint.lean b/Foundation/FirstOrder/Bootstrapping/FixedPoint.lean index ca0d1bc66..150849d53 100644 --- a/Foundation/FirstOrder/Bootstrapping/FixedPoint.lean +++ b/Foundation/FirstOrder/Bootstrapping/FixedPoint.lean @@ -1,7 +1,6 @@ module -public import Foundation.FirstOrder.Arithmetic.Basic.Model -public import Foundation.FirstOrder.Bootstrapping.Syntax +public import Foundation.FirstOrder.Bootstrapping.Syntax.Proof.Coding @[expose] public section open Classical diff --git a/Foundation/FirstOrder/Bootstrapping/Syntax.lean b/Foundation/FirstOrder/Bootstrapping/Syntax.lean deleted file mode 100644 index 498efc059..000000000 --- a/Foundation/FirstOrder/Bootstrapping/Syntax.lean +++ /dev/null @@ -1,16 +0,0 @@ -module - -public import Foundation.FirstOrder.Bootstrapping.Syntax.Language -public import Foundation.FirstOrder.Bootstrapping.Syntax.Term.Basic -public import Foundation.FirstOrder.Bootstrapping.Syntax.Term.Functions -public import Foundation.FirstOrder.Bootstrapping.Syntax.Term.Typed -public import Foundation.FirstOrder.Bootstrapping.Syntax.Term.Coding -public import Foundation.FirstOrder.Bootstrapping.Syntax.Formula.Basic -public import Foundation.FirstOrder.Bootstrapping.Syntax.Formula.Functions -public import Foundation.FirstOrder.Bootstrapping.Syntax.Formula.Iteration -public import Foundation.FirstOrder.Bootstrapping.Syntax.Formula.Typed -public import Foundation.FirstOrder.Bootstrapping.Syntax.Formula.Coding -public import Foundation.FirstOrder.Bootstrapping.Syntax.Theory -public import Foundation.FirstOrder.Bootstrapping.Syntax.Proof.Basic -public import Foundation.FirstOrder.Bootstrapping.Syntax.Proof.Typed -public import Foundation.FirstOrder.Bootstrapping.Syntax.Proof.Coding \ No newline at end of file diff --git a/Foundation/FirstOrder/Bootstrapping/Syntax/Language.lean b/Foundation/FirstOrder/Bootstrapping/Syntax/Language.lean index 61db8e8c6..049e0b56a 100644 --- a/Foundation/FirstOrder/Bootstrapping/Syntax/Language.lean +++ b/Foundation/FirstOrder/Bootstrapping/Syntax/Language.lean @@ -1,6 +1,6 @@ module -public import Foundation.FirstOrder.Arithmetic.HFS +public import Foundation.FirstOrder.Arithmetic.HFS.Coding @[expose] public section /-! # Internalized languages of first-order logic -/ diff --git a/Foundation/FirstOrder/Completeness.lean b/Foundation/FirstOrder/Completeness.lean deleted file mode 100644 index 77aa99aa0..000000000 --- a/Foundation/FirstOrder/Completeness.lean +++ /dev/null @@ -1,5 +0,0 @@ -module - -public import Foundation.FirstOrder.Completeness.CanonicalModel -public import Foundation.FirstOrder.Completeness.CountableSublanguage -public import Foundation.FirstOrder.Completeness.CounterModel diff --git a/Foundation/FirstOrder/Completeness/CountableSublanguage.lean b/Foundation/FirstOrder/Completeness/CountableSublanguage.lean index 2345c8641..7674482b1 100644 --- a/Foundation/FirstOrder/Completeness/CountableSublanguage.lean +++ b/Foundation/FirstOrder/Completeness/CountableSublanguage.lean @@ -1,6 +1,12 @@ module -public import Foundation.FirstOrder.Basic +public import Foundation.FirstOrder.Basic.Model +public import Foundation.FirstOrder.Basic.CutFree +public import Foundation.FirstOrder.Basic.Calculus2 +public import Foundation.FirstOrder.Basic.Coding +public import Foundation.FirstOrder.Basic.Eq +public import Foundation.FirstOrder.Basic.Padding +public import Foundation.FirstOrder.Basic.Definability public import Mathlib.Logic.Equiv.List @[expose] public section diff --git a/Foundation/FirstOrder/Completeness/CounterModel.lean b/Foundation/FirstOrder/Completeness/CounterModel.lean index 83ef52698..476302d2d 100644 --- a/Foundation/FirstOrder/Completeness/CounterModel.lean +++ b/Foundation/FirstOrder/Completeness/CounterModel.lean @@ -4,8 +4,6 @@ public import Foundation.FirstOrder.Completeness.CanonicalModel public import Foundation.FirstOrder.Completeness.CountableSublanguage public import Foundation.FirstOrder.Ultraproduct public import Foundation.Vorspiel.Order.Dense -public import Mathlib.Logic.Equiv.List -public import Mathlib.Logic.Encodable.Basic /-! # Completeness theorem -/ diff --git a/Foundation/FirstOrder/Incompleteness/ProvabilityAbstraction/Basic.lean b/Foundation/FirstOrder/Incompleteness/ProvabilityAbstraction/Basic.lean index 692ff47e6..10116b736 100644 --- a/Foundation/FirstOrder/Incompleteness/ProvabilityAbstraction/Basic.lean +++ b/Foundation/FirstOrder/Incompleteness/ProvabilityAbstraction/Basic.lean @@ -1,6 +1,7 @@ module -public import Foundation.FirstOrder.Arithmetic.Basic +public import Foundation.FirstOrder.Arithmetic.Basic.Monotone +public import Foundation.FirstOrder.Arithmetic.Basic.Hierarchy public import Foundation.Meta.ClProver @[expose] public section diff --git a/Foundation/FirstOrder/Intuitionistic/Formula.lean b/Foundation/FirstOrder/Intuitionistic/Formula.lean index 7da9c060e..73532e27d 100644 --- a/Foundation/FirstOrder/Intuitionistic/Formula.lean +++ b/Foundation/FirstOrder/Intuitionistic/Formula.lean @@ -1,6 +1,12 @@ module -public import Foundation.FirstOrder.Basic +public import Foundation.FirstOrder.Basic.Model +public import Foundation.FirstOrder.Basic.CutFree +public import Foundation.FirstOrder.Basic.Calculus2 +public import Foundation.FirstOrder.Basic.Coding +public import Foundation.FirstOrder.Basic.Eq +public import Foundation.FirstOrder.Basic.Padding +public import Foundation.FirstOrder.Basic.Definability @[expose] public section /-! diff --git a/Foundation/FirstOrder/Kripke/Basic.lean b/Foundation/FirstOrder/Kripke/Basic.lean index d76f33ccb..5c30d13f5 100644 --- a/Foundation/FirstOrder/Kripke/Basic.lean +++ b/Foundation/FirstOrder/Kripke/Basic.lean @@ -1,6 +1,12 @@ module -public import Foundation.FirstOrder.Basic +public import Foundation.FirstOrder.Basic.Model +public import Foundation.FirstOrder.Basic.CutFree +public import Foundation.FirstOrder.Basic.Calculus2 +public import Foundation.FirstOrder.Basic.Coding +public import Foundation.FirstOrder.Basic.Eq +public import Foundation.FirstOrder.Basic.Padding +public import Foundation.FirstOrder.Basic.Definability public import Foundation.Syntax.Predicate.Relational public import Foundation.Logic.ForcingRelation public import Foundation.Vorspiel.Order.Dense diff --git a/Foundation/FirstOrder/Order/Le.lean b/Foundation/FirstOrder/Order/Le.lean index dc3b192f1..52de27960 100644 --- a/Foundation/FirstOrder/Order/Le.lean +++ b/Foundation/FirstOrder/Order/Le.lean @@ -1,6 +1,6 @@ module -public import Foundation.FirstOrder.Completeness +public import Foundation.FirstOrder.Completeness.CounterModel @[expose] public section namespace LO diff --git a/Foundation/FirstOrder/Polarity.lean b/Foundation/FirstOrder/Polarity.lean index fadeea0c9..d7fbfa0fb 100644 --- a/Foundation/FirstOrder/Polarity.lean +++ b/Foundation/FirstOrder/Polarity.lean @@ -1,6 +1,12 @@ module -public import Foundation.FirstOrder.Basic +public import Foundation.FirstOrder.Basic.Model +public import Foundation.FirstOrder.Basic.CutFree +public import Foundation.FirstOrder.Basic.Calculus2 +public import Foundation.FirstOrder.Basic.Coding +public import Foundation.FirstOrder.Basic.Eq +public import Foundation.FirstOrder.Basic.Padding +public import Foundation.FirstOrder.Basic.Definability /-! # Polarity of formulas diff --git a/Foundation/FirstOrder/SetTheory/Basic.lean b/Foundation/FirstOrder/SetTheory/Basic.lean deleted file mode 100644 index d75faa64a..000000000 --- a/Foundation/FirstOrder/SetTheory/Basic.lean +++ /dev/null @@ -1,5 +0,0 @@ -module - -public import Foundation.FirstOrder.SetTheory.Basic.Misc -public import Foundation.FirstOrder.SetTheory.Basic.Axioms -public import Foundation.FirstOrder.SetTheory.Basic.Model \ No newline at end of file diff --git a/Foundation/FirstOrder/SetTheory/LoewenheimSkolem.lean b/Foundation/FirstOrder/SetTheory/LoewenheimSkolem.lean index 14d0f7845..df5d64b90 100644 --- a/Foundation/FirstOrder/SetTheory/LoewenheimSkolem.lean +++ b/Foundation/FirstOrder/SetTheory/LoewenheimSkolem.lean @@ -1,6 +1,6 @@ module -public import Foundation.FirstOrder.SetTheory.Basic +public import Foundation.FirstOrder.SetTheory.Basic.Model public import Foundation.FirstOrder.Skolemization.Hull @[expose] public section diff --git a/Foundation/FirstOrder/SetTheory/Universe.lean b/Foundation/FirstOrder/SetTheory/Universe.lean index 9d5c11e1d..7f0841be3 100644 --- a/Foundation/FirstOrder/SetTheory/Universe.lean +++ b/Foundation/FirstOrder/SetTheory/Universe.lean @@ -1,6 +1,6 @@ module -public import Foundation.FirstOrder.SetTheory.Basic +public import Foundation.FirstOrder.SetTheory.Basic.Model public import Mathlib.Data.QPF.Univariate.Basic public import Mathlib.SetTheory.Cardinal.Aleph public import Foundation.Vorspiel.Small diff --git a/Foundation/FirstOrder/SetTheory/Z.lean b/Foundation/FirstOrder/SetTheory/Z.lean index 69b24afd5..37997c704 100644 --- a/Foundation/FirstOrder/SetTheory/Z.lean +++ b/Foundation/FirstOrder/SetTheory/Z.lean @@ -1,6 +1,6 @@ module -public import Foundation.FirstOrder.SetTheory.Basic +public import Foundation.FirstOrder.SetTheory.Basic.Model public import Foundation.Vorspiel.ExistsUnique /-! diff --git a/Foundation/FirstOrder/Skolemization/Hull.lean b/Foundation/FirstOrder/Skolemization/Hull.lean index e6b74def4..d22e6007e 100644 --- a/Foundation/FirstOrder/Skolemization/Hull.lean +++ b/Foundation/FirstOrder/Skolemization/Hull.lean @@ -1,6 +1,12 @@ module -public import Foundation.FirstOrder.Basic +public import Foundation.FirstOrder.Basic.Model +public import Foundation.FirstOrder.Basic.CutFree +public import Foundation.FirstOrder.Basic.Calculus2 +public import Foundation.FirstOrder.Basic.Coding +public import Foundation.FirstOrder.Basic.Eq +public import Foundation.FirstOrder.Basic.Padding +public import Foundation.FirstOrder.Basic.Definability public import Mathlib.SetTheory.Cardinal.Basic @[expose] public section diff --git a/Foundation/FirstOrder/Ultraproduct.lean b/Foundation/FirstOrder/Ultraproduct.lean index fa6ec0046..14ef69c4e 100644 --- a/Foundation/FirstOrder/Ultraproduct.lean +++ b/Foundation/FirstOrder/Ultraproduct.lean @@ -1,6 +1,12 @@ module -public import Foundation.FirstOrder.Basic +public import Foundation.FirstOrder.Basic.Model +public import Foundation.FirstOrder.Basic.CutFree +public import Foundation.FirstOrder.Basic.Calculus2 +public import Foundation.FirstOrder.Basic.Coding +public import Foundation.FirstOrder.Basic.Eq +public import Foundation.FirstOrder.Basic.Padding +public import Foundation.FirstOrder.Basic.Definability public import Mathlib.Order.Filter.Ultrafilter.Basic @[expose] public section diff --git a/Foundation/LinearLogic/FirstOrder/Formula.lean b/Foundation/LinearLogic/FirstOrder/Formula.lean index 2c7667f62..4bd306979 100644 --- a/Foundation/LinearLogic/FirstOrder/Formula.lean +++ b/Foundation/LinearLogic/FirstOrder/Formula.lean @@ -1,6 +1,12 @@ module -public import Foundation.FirstOrder.Basic +public import Foundation.FirstOrder.Basic.Model +public import Foundation.FirstOrder.Basic.CutFree +public import Foundation.FirstOrder.Basic.Calculus2 +public import Foundation.FirstOrder.Basic.Coding +public import Foundation.FirstOrder.Basic.Eq +public import Foundation.FirstOrder.Basic.Padding +public import Foundation.FirstOrder.Basic.Definability public import Foundation.LinearLogic.LogicSymbol /-! diff --git a/Foundation/Modal/VanBentham/StandardTranslation.lean b/Foundation/Modal/VanBentham/StandardTranslation.lean index 77b460b7d..d048db446 100644 --- a/Foundation/Modal/VanBentham/StandardTranslation.lean +++ b/Foundation/Modal/VanBentham/StandardTranslation.lean @@ -1,6 +1,12 @@ module -public import Foundation.FirstOrder.Basic +public import Foundation.FirstOrder.Basic.Model +public import Foundation.FirstOrder.Basic.CutFree +public import Foundation.FirstOrder.Basic.Calculus2 +public import Foundation.FirstOrder.Basic.Coding +public import Foundation.FirstOrder.Basic.Eq +public import Foundation.FirstOrder.Basic.Padding +public import Foundation.FirstOrder.Basic.Definability public import Foundation.Modal.Kripke.NNFormula @[expose] public section diff --git a/Foundation/SecondOrder/Syntax/Formula.lean b/Foundation/SecondOrder/Syntax/Formula.lean index b9c9b27ba..ded31982d 100644 --- a/Foundation/SecondOrder/Syntax/Formula.lean +++ b/Foundation/SecondOrder/Syntax/Formula.lean @@ -1,6 +1,12 @@ module -public import Foundation.FirstOrder.Basic +public import Foundation.FirstOrder.Basic.Model +public import Foundation.FirstOrder.Basic.CutFree +public import Foundation.FirstOrder.Basic.Calculus2 +public import Foundation.FirstOrder.Basic.Coding +public import Foundation.FirstOrder.Basic.Eq +public import Foundation.FirstOrder.Basic.Padding +public import Foundation.FirstOrder.Basic.Definability @[expose] public section diff --git a/Foundation/Vorspiel/NotationClass.lean b/Foundation/Vorspiel/NotationClass.lean index e1cae7e10..c050f8559 100644 --- a/Foundation/Vorspiel/NotationClass.lean +++ b/Foundation/Vorspiel/NotationClass.lean @@ -1,6 +1,5 @@ module -public import Mathlib.Tactic.TypeStar public import Mathlib.Data.Nat.Basic /-!