Skip to content

refactor: remove import-only aggregator files #839

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
SnO2WMaN wants to merge 2 commits into
base: master
Choose a base branch
from
Open

refactor: remove import-only aggregator files #839

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
5b03e4b
refactor: remove import-only aggregator files
SnO2WMaN Jul 8, 2026
fe4cf49
refactor: shake unused imports from the aggregator-removal diff
SnO2WMaN Jul 8, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 0 additions & 8 deletions Foundation.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down
6 changes: 0 additions & 6 deletions Foundation/FirstOrder/Arithmetic/Basic.lean
View file
Open in desktop

This file was deleted.

6 changes: 0 additions & 6 deletions Foundation/FirstOrder/Arithmetic/Definability.lean
View file
Open in desktop

This file was deleted.

7 changes: 0 additions & 7 deletions Foundation/FirstOrder/Arithmetic/Exponential.lean
View file
Open in desktop

This file was deleted.

1 change: 0 additions & 1 deletion Foundation/FirstOrder/Arithmetic/Exponential/Exp.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
module

public import Foundation.FirstOrder.Arithmetic.Exponential.PPow2
public import Mathlib.Algebra.Order.Ring.Basic

@[expose] public section
/-!
Expand Down
8 changes: 0 additions & 8 deletions Foundation/FirstOrder/Arithmetic/HFS.lean
View file
Open in desktop

This file was deleted.

2 changes: 1 addition & 1 deletion Foundation/FirstOrder/Arithmetic/HFS/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
module

public import Foundation.FirstOrder.Arithmetic.Exponential
public import Foundation.FirstOrder.Arithmetic.Exponential.Bit

@[expose] public section
/-!
Expand Down
2 changes: 1 addition & 1 deletion Foundation/FirstOrder/Arithmetic/Induction.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
module

public import Foundation.FirstOrder.Arithmetic.HFS
public import Foundation.FirstOrder.Arithmetic.HFS.Coding

@[expose] public section
/-!
Expand Down
2 changes: 1 addition & 1 deletion Foundation/FirstOrder/Arithmetic/Omega1/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
module

public import Foundation.FirstOrder.Arithmetic.Exponential
public import Foundation.FirstOrder.Arithmetic.Exponential.Bit

@[expose] public section
/-!
Expand Down
2 changes: 1 addition & 1 deletion Foundation/FirstOrder/Arithmetic/PeanoMinus/Functions.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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

Expand Down
3 changes: 2 additions & 1 deletion Foundation/FirstOrder/Arithmetic/R0/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
/-!
Expand Down
3 changes: 2 additions & 1 deletion Foundation/FirstOrder/Arithmetic/TA/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
17 changes: 0 additions & 17 deletions Foundation/FirstOrder/Basic.lean
View file
Open in desktop

This file was deleted.

1 change: 0 additions & 1 deletion Foundation/FirstOrder/Basic/Calculus.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D1.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
module

public import Foundation.FirstOrder.Bootstrapping.Syntax
public import Foundation.FirstOrder.Bootstrapping.Syntax.Proof.Coding

@[expose] public section
/-!
Expand Down
2 changes: 1 addition & 1 deletion Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D2.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
module

public import Foundation.FirstOrder.Bootstrapping.Syntax
public import Foundation.FirstOrder.Bootstrapping.Syntax.Proof.Coding

@[expose] public section
/-!
Expand Down
3 changes: 1 addition & 2 deletions Foundation/FirstOrder/Bootstrapping/FixedPoint.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
16 changes: 0 additions & 16 deletions Foundation/FirstOrder/Bootstrapping/Syntax.lean
View file
Open in desktop

This file was deleted.

2 changes: 1 addition & 1 deletion Foundation/FirstOrder/Bootstrapping/Syntax/Language.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 -/
Expand Down
5 changes: 0 additions & 5 deletions Foundation/FirstOrder/Completeness.lean
View file
Open in desktop

This file was deleted.

8 changes: 7 additions & 1 deletion Foundation/FirstOrder/Completeness/CountableSublanguage.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
2 changes: 0 additions & 2 deletions Foundation/FirstOrder/Completeness/CounterModel.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 -/

Expand Down
3 changes: 2 additions & 1 deletion Foundation/FirstOrder/Incompleteness/ProvabilityAbstraction/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
8 changes: 7 additions & 1 deletion Foundation/FirstOrder/Intuitionistic/Formula.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
/-!
Expand Down
8 changes: 7 additions & 1 deletion Foundation/FirstOrder/Kripke/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
2 changes: 1 addition & 1 deletion Foundation/FirstOrder/Order/Le.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
module

public import Foundation.FirstOrder.Completeness
public import Foundation.FirstOrder.Completeness.CounterModel

@[expose] public section
namespace LO
Expand Down
8 changes: 7 additions & 1 deletion Foundation/FirstOrder/Polarity.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
5 changes: 0 additions & 5 deletions Foundation/FirstOrder/SetTheory/Basic.lean
View file
Open in desktop

This file was deleted.

2 changes: 1 addition & 1 deletion Foundation/FirstOrder/SetTheory/LoewenheimSkolem.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
2 changes: 1 addition & 1 deletion Foundation/FirstOrder/SetTheory/Universe.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
2 changes: 1 addition & 1 deletion Foundation/FirstOrder/SetTheory/Z.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
module

public import Foundation.FirstOrder.SetTheory.Basic
public import Foundation.FirstOrder.SetTheory.Basic.Model
public import Foundation.Vorspiel.ExistsUnique

/-!
Expand Down
8 changes: 7 additions & 1 deletion Foundation/FirstOrder/Skolemization/Hull.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
8 changes: 7 additions & 1 deletion Foundation/FirstOrder/Ultraproduct.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
8 changes: 7 additions & 1 deletion Foundation/LinearLogic/FirstOrder/Formula.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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

/-!
Expand Down
8 changes: 7 additions & 1 deletion Foundation/Modal/VanBentham/StandardTranslation.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
Loading
Loading