From 5b03e4bc630499d8b950430cce6fff349e20a14c Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Wed, 8 Jul 2026 19:33:11 +0900 Subject: [PATCH 1/2] refactor: remove import-only aggregator files Delete Lean modules that only re-export their submodules via `public import` (Foundation/FirstOrder/Basic.lean, Foundation/FirstOrder/Completeness.lean, Foundation/FirstOrder/Bootstrapping/Syntax.lean, Foundation/FirstOrder/SetTheory/Basic.lean, Foundation/FirstOrder/Arithmetic/{HFS,Definability,Exponential,Basic}.lean) and inline their import lists into the files that imported them. Foundation.lean is regenerated via `lake exe mk_all --module`. --- Foundation.lean | 8 -------- Foundation/FirstOrder/Arithmetic/Basic.lean | 6 ------ .../FirstOrder/Arithmetic/Definability.lean | 6 ------ .../FirstOrder/Arithmetic/Exponential.lean | 7 ------- Foundation/FirstOrder/Arithmetic/HFS.lean | 8 -------- Foundation/FirstOrder/Arithmetic/HFS/Basic.lean | 6 +++++- Foundation/FirstOrder/Arithmetic/Induction.lean | 7 ++++++- .../FirstOrder/Arithmetic/Omega1/Basic.lean | 6 +++++- .../Arithmetic/PeanoMinus/Functions.lean | 5 ++++- Foundation/FirstOrder/Arithmetic/R0/Basic.lean | 5 ++++- Foundation/FirstOrder/Arithmetic/TA/Basic.lean | 5 ++++- Foundation/FirstOrder/Basic.lean | 17 ----------------- .../Bootstrapping/DerivabilityCondition/D1.lean | 15 ++++++++++++++- .../Bootstrapping/DerivabilityCondition/D2.lean | 15 ++++++++++++++- .../FirstOrder/Bootstrapping/FixedPoint.lean | 15 ++++++++++++++- Foundation/FirstOrder/Bootstrapping/Syntax.lean | 16 ---------------- .../Bootstrapping/Syntax/Language.lean | 7 ++++++- Foundation/FirstOrder/Completeness.lean | 5 ----- .../Completeness/CountableSublanguage.lean | 16 +++++++++++++++- .../ProvabilityAbstraction/Basic.lean | 5 ++++- .../FirstOrder/Intuitionistic/Formula.lean | 16 +++++++++++++++- Foundation/FirstOrder/Kripke/Basic.lean | 16 +++++++++++++++- Foundation/FirstOrder/Order/Le.lean | 4 +++- Foundation/FirstOrder/Polarity.lean | 16 +++++++++++++++- Foundation/FirstOrder/SetTheory/Basic.lean | 5 ----- .../FirstOrder/SetTheory/LoewenheimSkolem.lean | 4 +++- Foundation/FirstOrder/SetTheory/Universe.lean | 4 +++- Foundation/FirstOrder/SetTheory/Z.lean | 4 +++- Foundation/FirstOrder/Skolemization/Hull.lean | 16 +++++++++++++++- Foundation/FirstOrder/Ultraproduct.lean | 16 +++++++++++++++- Foundation/LinearLogic/FirstOrder/Formula.lean | 16 +++++++++++++++- .../Modal/VanBentham/StandardTranslation.lean | 16 +++++++++++++++- Foundation/SecondOrder/Syntax/Formula.lean | 16 +++++++++++++++- 33 files changed, 227 insertions(+), 102 deletions(-) delete mode 100644 Foundation/FirstOrder/Arithmetic/Basic.lean delete mode 100644 Foundation/FirstOrder/Arithmetic/Definability.lean delete mode 100644 Foundation/FirstOrder/Arithmetic/Exponential.lean delete mode 100644 Foundation/FirstOrder/Arithmetic/HFS.lean delete mode 100644 Foundation/FirstOrder/Basic.lean delete mode 100644 Foundation/FirstOrder/Bootstrapping/Syntax.lean delete mode 100644 Foundation/FirstOrder/Completeness.lean delete mode 100644 Foundation/FirstOrder/SetTheory/Basic.lean 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/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..db3d62ac3 100644 --- a/Foundation/FirstOrder/Arithmetic/HFS/Basic.lean +++ b/Foundation/FirstOrder/Arithmetic/HFS/Basic.lean @@ -1,6 +1,10 @@ module -public import Foundation.FirstOrder.Arithmetic.Exponential +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 @[expose] public section /-! diff --git a/Foundation/FirstOrder/Arithmetic/Induction.lean b/Foundation/FirstOrder/Arithmetic/Induction.lean index 2608035c0..4d1da5eb5 100644 --- a/Foundation/FirstOrder/Arithmetic/Induction.lean +++ b/Foundation/FirstOrder/Arithmetic/Induction.lean @@ -1,6 +1,11 @@ module -public import Foundation.FirstOrder.Arithmetic.HFS +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 @[expose] public section /-! diff --git a/Foundation/FirstOrder/Arithmetic/Omega1/Basic.lean b/Foundation/FirstOrder/Arithmetic/Omega1/Basic.lean index 71af62bf2..b56084be1 100644 --- a/Foundation/FirstOrder/Arithmetic/Omega1/Basic.lean +++ b/Foundation/FirstOrder/Arithmetic/Omega1/Basic.lean @@ -1,6 +1,10 @@ module -public import Foundation.FirstOrder.Arithmetic.Exponential +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 @[expose] public section /-! diff --git a/Foundation/FirstOrder/Arithmetic/PeanoMinus/Functions.lean b/Foundation/FirstOrder/Arithmetic/PeanoMinus/Functions.lean index bb6ac9e18..b2297de0f 100644 --- a/Foundation/FirstOrder/Arithmetic/PeanoMinus/Functions.lean +++ b/Foundation/FirstOrder/Arithmetic/PeanoMinus/Functions.lean @@ -1,6 +1,9 @@ module -public import Foundation.FirstOrder.Arithmetic.Definability +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 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..be7bcd196 100644 --- a/Foundation/FirstOrder/Arithmetic/R0/Basic.lean +++ b/Foundation/FirstOrder/Arithmetic/R0/Basic.lean @@ -1,6 +1,9 @@ module -public import Foundation.FirstOrder.Arithmetic.Basic +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 @[expose] public section /-! diff --git a/Foundation/FirstOrder/Arithmetic/TA/Basic.lean b/Foundation/FirstOrder/Arithmetic/TA/Basic.lean index 52b63dc24..bd458e578 100644 --- a/Foundation/FirstOrder/Arithmetic/TA/Basic.lean +++ b/Foundation/FirstOrder/Arithmetic/TA/Basic.lean @@ -1,6 +1,9 @@ module -public import Foundation.FirstOrder.Arithmetic.Basic +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 @[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/Bootstrapping/DerivabilityCondition/D1.lean b/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D1.lean index 32c52217d..33f0bcd86 100644 --- a/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D1.lean +++ b/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D1.lean @@ -1,6 +1,19 @@ module -public import Foundation.FirstOrder.Bootstrapping.Syntax +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 @[expose] public section /-! diff --git a/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D2.lean b/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D2.lean index e817e9692..398552784 100644 --- a/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D2.lean +++ b/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D2.lean @@ -1,6 +1,19 @@ module -public import Foundation.FirstOrder.Bootstrapping.Syntax +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 @[expose] public section /-! diff --git a/Foundation/FirstOrder/Bootstrapping/FixedPoint.lean b/Foundation/FirstOrder/Bootstrapping/FixedPoint.lean index ca0d1bc66..41754d946 100644 --- a/Foundation/FirstOrder/Bootstrapping/FixedPoint.lean +++ b/Foundation/FirstOrder/Bootstrapping/FixedPoint.lean @@ -1,7 +1,20 @@ module public import Foundation.FirstOrder.Arithmetic.Basic.Model -public import Foundation.FirstOrder.Bootstrapping.Syntax +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 @[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..bfe68b369 100644 --- a/Foundation/FirstOrder/Bootstrapping/Syntax/Language.lean +++ b/Foundation/FirstOrder/Bootstrapping/Syntax/Language.lean @@ -1,6 +1,11 @@ module -public import Foundation.FirstOrder.Arithmetic.HFS +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 @[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..e99096c0a 100644 --- a/Foundation/FirstOrder/Completeness/CountableSublanguage.lean +++ b/Foundation/FirstOrder/Completeness/CountableSublanguage.lean @@ -1,6 +1,20 @@ module -public import Foundation.FirstOrder.Basic +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 public import Mathlib.Logic.Equiv.List @[expose] public section diff --git a/Foundation/FirstOrder/Incompleteness/ProvabilityAbstraction/Basic.lean b/Foundation/FirstOrder/Incompleteness/ProvabilityAbstraction/Basic.lean index 692ff47e6..34b0a866c 100644 --- a/Foundation/FirstOrder/Incompleteness/ProvabilityAbstraction/Basic.lean +++ b/Foundation/FirstOrder/Incompleteness/ProvabilityAbstraction/Basic.lean @@ -1,6 +1,9 @@ module -public import Foundation.FirstOrder.Arithmetic.Basic +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 public import Foundation.Meta.ClProver @[expose] public section diff --git a/Foundation/FirstOrder/Intuitionistic/Formula.lean b/Foundation/FirstOrder/Intuitionistic/Formula.lean index 7da9c060e..5c71043aa 100644 --- a/Foundation/FirstOrder/Intuitionistic/Formula.lean +++ b/Foundation/FirstOrder/Intuitionistic/Formula.lean @@ -1,6 +1,20 @@ module -public import Foundation.FirstOrder.Basic +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 @[expose] public section /-! diff --git a/Foundation/FirstOrder/Kripke/Basic.lean b/Foundation/FirstOrder/Kripke/Basic.lean index d76f33ccb..29edb0b50 100644 --- a/Foundation/FirstOrder/Kripke/Basic.lean +++ b/Foundation/FirstOrder/Kripke/Basic.lean @@ -1,6 +1,20 @@ module -public import Foundation.FirstOrder.Basic +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 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..7fbba4e1f 100644 --- a/Foundation/FirstOrder/Order/Le.lean +++ b/Foundation/FirstOrder/Order/Le.lean @@ -1,6 +1,8 @@ module -public import Foundation.FirstOrder.Completeness +public import Foundation.FirstOrder.Completeness.CanonicalModel +public import Foundation.FirstOrder.Completeness.CountableSublanguage +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..20b2548a1 100644 --- a/Foundation/FirstOrder/Polarity.lean +++ b/Foundation/FirstOrder/Polarity.lean @@ -1,6 +1,20 @@ module -public import Foundation.FirstOrder.Basic +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 /-! # 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..1a78b4907 100644 --- a/Foundation/FirstOrder/SetTheory/LoewenheimSkolem.lean +++ b/Foundation/FirstOrder/SetTheory/LoewenheimSkolem.lean @@ -1,6 +1,8 @@ module -public import Foundation.FirstOrder.SetTheory.Basic +public import Foundation.FirstOrder.SetTheory.Basic.Misc +public import Foundation.FirstOrder.SetTheory.Basic.Axioms +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..e4a847056 100644 --- a/Foundation/FirstOrder/SetTheory/Universe.lean +++ b/Foundation/FirstOrder/SetTheory/Universe.lean @@ -1,6 +1,8 @@ module -public import Foundation.FirstOrder.SetTheory.Basic +public import Foundation.FirstOrder.SetTheory.Basic.Misc +public import Foundation.FirstOrder.SetTheory.Basic.Axioms +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..0b12cc99a 100644 --- a/Foundation/FirstOrder/SetTheory/Z.lean +++ b/Foundation/FirstOrder/SetTheory/Z.lean @@ -1,6 +1,8 @@ module -public import Foundation.FirstOrder.SetTheory.Basic +public import Foundation.FirstOrder.SetTheory.Basic.Misc +public import Foundation.FirstOrder.SetTheory.Basic.Axioms +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..1be3a3d18 100644 --- a/Foundation/FirstOrder/Skolemization/Hull.lean +++ b/Foundation/FirstOrder/Skolemization/Hull.lean @@ -1,6 +1,20 @@ module -public import Foundation.FirstOrder.Basic +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 public import Mathlib.SetTheory.Cardinal.Basic @[expose] public section diff --git a/Foundation/FirstOrder/Ultraproduct.lean b/Foundation/FirstOrder/Ultraproduct.lean index fa6ec0046..8099a6170 100644 --- a/Foundation/FirstOrder/Ultraproduct.lean +++ b/Foundation/FirstOrder/Ultraproduct.lean @@ -1,6 +1,20 @@ module -public import Foundation.FirstOrder.Basic +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 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..4aa8afdd1 100644 --- a/Foundation/LinearLogic/FirstOrder/Formula.lean +++ b/Foundation/LinearLogic/FirstOrder/Formula.lean @@ -1,6 +1,20 @@ module -public import Foundation.FirstOrder.Basic +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 public import Foundation.LinearLogic.LogicSymbol /-! diff --git a/Foundation/Modal/VanBentham/StandardTranslation.lean b/Foundation/Modal/VanBentham/StandardTranslation.lean index 77b460b7d..0041c1566 100644 --- a/Foundation/Modal/VanBentham/StandardTranslation.lean +++ b/Foundation/Modal/VanBentham/StandardTranslation.lean @@ -1,6 +1,20 @@ module -public import Foundation.FirstOrder.Basic +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 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..020b37868 100644 --- a/Foundation/SecondOrder/Syntax/Formula.lean +++ b/Foundation/SecondOrder/Syntax/Formula.lean @@ -1,6 +1,20 @@ module -public import Foundation.FirstOrder.Basic +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 @[expose] public section From fe4cf491d3633e448d1047b216c8a48aea9708be Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Wed, 8 Jul 2026 20:46:07 +0900 Subject: [PATCH 2/2] refactor: shake unused imports from the aggregator-removal diff Run `lake shake --keep-public --fix` over the files touched by the previous commit to drop imports that turned out to be unused after inlining the deleted aggregator files' import lists. `--keep-public` avoids downgrading still-needed `public import`s to private ones, which would silently break downstream re-exports (e.g. `cl_prover` via Foundation.Meta.ClProver, and Finset's `Repr` instance). Co-Authored-By: Claude --- .../FirstOrder/Arithmetic/Exponential/Exp.lean | 1 - Foundation/FirstOrder/Arithmetic/HFS/Basic.lean | 4 ---- Foundation/FirstOrder/Arithmetic/Induction.lean | 5 ----- Foundation/FirstOrder/Arithmetic/Omega1/Basic.lean | 4 ---- .../Arithmetic/PeanoMinus/Functions.lean | 3 --- Foundation/FirstOrder/Arithmetic/R0/Basic.lean | 2 -- Foundation/FirstOrder/Arithmetic/TA/Basic.lean | 2 -- Foundation/FirstOrder/Basic/Calculus.lean | 1 - .../Bootstrapping/DerivabilityCondition/D1.lean | 13 ------------- .../Bootstrapping/DerivabilityCondition/D2.lean | 13 ------------- .../FirstOrder/Bootstrapping/FixedPoint.lean | 14 -------------- .../FirstOrder/Bootstrapping/Syntax/Language.lean | 5 ----- .../Completeness/CountableSublanguage.lean | 8 -------- .../FirstOrder/Completeness/CounterModel.lean | 2 -- .../ProvabilityAbstraction/Basic.lean | 2 -- Foundation/FirstOrder/Intuitionistic/Formula.lean | 8 -------- Foundation/FirstOrder/Kripke/Basic.lean | 8 -------- Foundation/FirstOrder/Order/Le.lean | 2 -- Foundation/FirstOrder/Polarity.lean | 8 -------- .../FirstOrder/SetTheory/LoewenheimSkolem.lean | 2 -- Foundation/FirstOrder/SetTheory/Universe.lean | 2 -- Foundation/FirstOrder/SetTheory/Z.lean | 2 -- Foundation/FirstOrder/Skolemization/Hull.lean | 8 -------- Foundation/FirstOrder/Ultraproduct.lean | 8 -------- Foundation/LinearLogic/FirstOrder/Formula.lean | 8 -------- .../Modal/VanBentham/StandardTranslation.lean | 8 -------- Foundation/SecondOrder/Syntax/Formula.lean | 8 -------- Foundation/Vorspiel/NotationClass.lean | 1 - 28 files changed, 152 deletions(-) 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/Basic.lean b/Foundation/FirstOrder/Arithmetic/HFS/Basic.lean index db3d62ac3..ba5cfe8c0 100644 --- a/Foundation/FirstOrder/Arithmetic/HFS/Basic.lean +++ b/Foundation/FirstOrder/Arithmetic/HFS/Basic.lean @@ -1,9 +1,5 @@ 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 @[expose] public section diff --git a/Foundation/FirstOrder/Arithmetic/Induction.lean b/Foundation/FirstOrder/Arithmetic/Induction.lean index 4d1da5eb5..b7ee07c07 100644 --- a/Foundation/FirstOrder/Arithmetic/Induction.lean +++ b/Foundation/FirstOrder/Arithmetic/Induction.lean @@ -1,10 +1,5 @@ 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 @[expose] public section diff --git a/Foundation/FirstOrder/Arithmetic/Omega1/Basic.lean b/Foundation/FirstOrder/Arithmetic/Omega1/Basic.lean index b56084be1..9d5c5a397 100644 --- a/Foundation/FirstOrder/Arithmetic/Omega1/Basic.lean +++ b/Foundation/FirstOrder/Arithmetic/Omega1/Basic.lean @@ -1,9 +1,5 @@ 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 @[expose] public section diff --git a/Foundation/FirstOrder/Arithmetic/PeanoMinus/Functions.lean b/Foundation/FirstOrder/Arithmetic/PeanoMinus/Functions.lean index b2297de0f..1c8725d25 100644 --- a/Foundation/FirstOrder/Arithmetic/PeanoMinus/Functions.lean +++ b/Foundation/FirstOrder/Arithmetic/PeanoMinus/Functions.lean @@ -1,8 +1,5 @@ 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 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 be7bcd196..01efc8216 100644 --- a/Foundation/FirstOrder/Arithmetic/R0/Basic.lean +++ b/Foundation/FirstOrder/Arithmetic/R0/Basic.lean @@ -1,9 +1,7 @@ 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 @[expose] public section /-! diff --git a/Foundation/FirstOrder/Arithmetic/TA/Basic.lean b/Foundation/FirstOrder/Arithmetic/TA/Basic.lean index bd458e578..a8ddb8878 100644 --- a/Foundation/FirstOrder/Arithmetic/TA/Basic.lean +++ b/Foundation/FirstOrder/Arithmetic/TA/Basic.lean @@ -1,9 +1,7 @@ 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 @[expose] public section namespace LO.FirstOrder.Arithmetic 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 33f0bcd86..cb149383f 100644 --- a/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D1.lean +++ b/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D1.lean @@ -1,18 +1,5 @@ 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 @[expose] public section diff --git a/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D2.lean b/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D2.lean index 398552784..40e881867 100644 --- a/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D2.lean +++ b/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D2.lean @@ -1,18 +1,5 @@ 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 @[expose] public section diff --git a/Foundation/FirstOrder/Bootstrapping/FixedPoint.lean b/Foundation/FirstOrder/Bootstrapping/FixedPoint.lean index 41754d946..150849d53 100644 --- a/Foundation/FirstOrder/Bootstrapping/FixedPoint.lean +++ b/Foundation/FirstOrder/Bootstrapping/FixedPoint.lean @@ -1,19 +1,5 @@ module -public import Foundation.FirstOrder.Arithmetic.Basic.Model -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 @[expose] public section diff --git a/Foundation/FirstOrder/Bootstrapping/Syntax/Language.lean b/Foundation/FirstOrder/Bootstrapping/Syntax/Language.lean index bfe68b369..049e0b56a 100644 --- a/Foundation/FirstOrder/Bootstrapping/Syntax/Language.lean +++ b/Foundation/FirstOrder/Bootstrapping/Syntax/Language.lean @@ -1,10 +1,5 @@ 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 @[expose] public section diff --git a/Foundation/FirstOrder/Completeness/CountableSublanguage.lean b/Foundation/FirstOrder/Completeness/CountableSublanguage.lean index e99096c0a..7674482b1 100644 --- a/Foundation/FirstOrder/Completeness/CountableSublanguage.lean +++ b/Foundation/FirstOrder/Completeness/CountableSublanguage.lean @@ -1,18 +1,10 @@ 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 public import Mathlib.Logic.Equiv.List 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 34b0a866c..10116b736 100644 --- a/Foundation/FirstOrder/Incompleteness/ProvabilityAbstraction/Basic.lean +++ b/Foundation/FirstOrder/Incompleteness/ProvabilityAbstraction/Basic.lean @@ -1,9 +1,7 @@ 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 public import Foundation.Meta.ClProver @[expose] public section diff --git a/Foundation/FirstOrder/Intuitionistic/Formula.lean b/Foundation/FirstOrder/Intuitionistic/Formula.lean index 5c71043aa..73532e27d 100644 --- a/Foundation/FirstOrder/Intuitionistic/Formula.lean +++ b/Foundation/FirstOrder/Intuitionistic/Formula.lean @@ -1,18 +1,10 @@ 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/Kripke/Basic.lean b/Foundation/FirstOrder/Kripke/Basic.lean index 29edb0b50..5c30d13f5 100644 --- a/Foundation/FirstOrder/Kripke/Basic.lean +++ b/Foundation/FirstOrder/Kripke/Basic.lean @@ -1,18 +1,10 @@ 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 public import Foundation.Syntax.Predicate.Relational diff --git a/Foundation/FirstOrder/Order/Le.lean b/Foundation/FirstOrder/Order/Le.lean index 7fbba4e1f..52de27960 100644 --- a/Foundation/FirstOrder/Order/Le.lean +++ b/Foundation/FirstOrder/Order/Le.lean @@ -1,7 +1,5 @@ module -public import Foundation.FirstOrder.Completeness.CanonicalModel -public import Foundation.FirstOrder.Completeness.CountableSublanguage public import Foundation.FirstOrder.Completeness.CounterModel @[expose] public section diff --git a/Foundation/FirstOrder/Polarity.lean b/Foundation/FirstOrder/Polarity.lean index 20b2548a1..d7fbfa0fb 100644 --- a/Foundation/FirstOrder/Polarity.lean +++ b/Foundation/FirstOrder/Polarity.lean @@ -1,18 +1,10 @@ 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/SetTheory/LoewenheimSkolem.lean b/Foundation/FirstOrder/SetTheory/LoewenheimSkolem.lean index 1a78b4907..df5d64b90 100644 --- a/Foundation/FirstOrder/SetTheory/LoewenheimSkolem.lean +++ b/Foundation/FirstOrder/SetTheory/LoewenheimSkolem.lean @@ -1,7 +1,5 @@ module -public import Foundation.FirstOrder.SetTheory.Basic.Misc -public import Foundation.FirstOrder.SetTheory.Basic.Axioms public import Foundation.FirstOrder.SetTheory.Basic.Model public import Foundation.FirstOrder.Skolemization.Hull diff --git a/Foundation/FirstOrder/SetTheory/Universe.lean b/Foundation/FirstOrder/SetTheory/Universe.lean index e4a847056..7f0841be3 100644 --- a/Foundation/FirstOrder/SetTheory/Universe.lean +++ b/Foundation/FirstOrder/SetTheory/Universe.lean @@ -1,7 +1,5 @@ module -public import Foundation.FirstOrder.SetTheory.Basic.Misc -public import Foundation.FirstOrder.SetTheory.Basic.Axioms public import Foundation.FirstOrder.SetTheory.Basic.Model public import Mathlib.Data.QPF.Univariate.Basic public import Mathlib.SetTheory.Cardinal.Aleph diff --git a/Foundation/FirstOrder/SetTheory/Z.lean b/Foundation/FirstOrder/SetTheory/Z.lean index 0b12cc99a..37997c704 100644 --- a/Foundation/FirstOrder/SetTheory/Z.lean +++ b/Foundation/FirstOrder/SetTheory/Z.lean @@ -1,7 +1,5 @@ module -public import Foundation.FirstOrder.SetTheory.Basic.Misc -public import Foundation.FirstOrder.SetTheory.Basic.Axioms 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 1be3a3d18..d22e6007e 100644 --- a/Foundation/FirstOrder/Skolemization/Hull.lean +++ b/Foundation/FirstOrder/Skolemization/Hull.lean @@ -1,18 +1,10 @@ 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 public import Mathlib.SetTheory.Cardinal.Basic diff --git a/Foundation/FirstOrder/Ultraproduct.lean b/Foundation/FirstOrder/Ultraproduct.lean index 8099a6170..14ef69c4e 100644 --- a/Foundation/FirstOrder/Ultraproduct.lean +++ b/Foundation/FirstOrder/Ultraproduct.lean @@ -1,18 +1,10 @@ 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 public import Mathlib.Order.Filter.Ultrafilter.Basic diff --git a/Foundation/LinearLogic/FirstOrder/Formula.lean b/Foundation/LinearLogic/FirstOrder/Formula.lean index 4aa8afdd1..4bd306979 100644 --- a/Foundation/LinearLogic/FirstOrder/Formula.lean +++ b/Foundation/LinearLogic/FirstOrder/Formula.lean @@ -1,18 +1,10 @@ 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 public import Foundation.LinearLogic.LogicSymbol diff --git a/Foundation/Modal/VanBentham/StandardTranslation.lean b/Foundation/Modal/VanBentham/StandardTranslation.lean index 0041c1566..d048db446 100644 --- a/Foundation/Modal/VanBentham/StandardTranslation.lean +++ b/Foundation/Modal/VanBentham/StandardTranslation.lean @@ -1,18 +1,10 @@ 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 public import Foundation.Modal.Kripke.NNFormula diff --git a/Foundation/SecondOrder/Syntax/Formula.lean b/Foundation/SecondOrder/Syntax/Formula.lean index 020b37868..ded31982d 100644 --- a/Foundation/SecondOrder/Syntax/Formula.lean +++ b/Foundation/SecondOrder/Syntax/Formula.lean @@ -1,18 +1,10 @@ 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/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 /-!