diff --git a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean index bb9f9c8f1..15c5d70c5 100644 --- a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean +++ b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean @@ -8,8 +8,8 @@ module public import Cslib.Algorithms.Lean.TimeM public import Mathlib.Data.Nat.Cast.Order.Ring -public import Mathlib.Order.Lattice.Nat public import Mathlib.Data.Nat.Log +public import Mathlib.Order.Lattice.Nat /-! # MergeSort on a list diff --git a/Cslib/Computability/Languages/OmegaLanguage.lean b/Cslib/Computability/Languages/OmegaLanguage.lean index cd17e2101..a48fac2a4 100644 --- a/Cslib/Computability/Languages/OmegaLanguage.lean +++ b/Cslib/Computability/Languages/OmegaLanguage.lean @@ -8,8 +8,7 @@ module public import Cslib.Computability.Languages.Language public import Cslib.Foundations.Data.OmegaSequence.Flatten -public import Mathlib.Computability.Language -public import Mathlib.Order.CompleteBooleanAlgebra +public import Mathlib.Algebra.Order.Sub.Basic public import Mathlib.Order.Filter.AtTopBot.Defs /-! diff --git a/Cslib/Computability/Languages/OmegaRegularLanguage.lean b/Cslib/Computability/Languages/OmegaRegularLanguage.lean index 75e89deff..6153d6e16 100644 --- a/Cslib/Computability/Languages/OmegaRegularLanguage.lean +++ b/Cslib/Computability/Languages/OmegaRegularLanguage.lean @@ -12,9 +12,9 @@ public import Cslib.Computability.Automata.NA.BuchiInter public import Cslib.Computability.Automata.NA.Sum public import Cslib.Computability.Languages.Congruences.BuchiCongruence public import Cslib.Computability.Languages.ExampleEventuallyZero -public import Mathlib.SetTheory.Cardinal.NatCard public import Mathlib.Data.Finite.Sigma public import Mathlib.Logic.Equiv.Fin.Basic +public import Mathlib.SetTheory.Cardinal.NatCard /-! # ω-Regular languages diff --git a/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean b/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean index ffd15a590..30ec6463e 100644 --- a/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean +++ b/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean @@ -6,12 +6,10 @@ Authors: Fabrizio Montesi module -public import Cslib.Foundations.Relation.Defs -public import Cslib.Foundations.Data.RelatesInSteps public import Cslib.Computability.Automata.NA.Basic public import Cslib.Computability.Automata.Transducers.Transducer -public import Cslib.Foundations.Data.BiTape public import Cslib.Computability.Machines.Turing.SingleTape.Defs +public import Cslib.Foundations.Data.RelatesInSteps /-! # Single-Tape Nondeterministic Turing Machines (NTMs) diff --git a/Cslib/Crypto/Protocols/PerfectSecrecy/Basic.lean b/Cslib/Crypto/Protocols/PerfectSecrecy/Basic.lean index c5f5a29ef..a68c42ee7 100644 --- a/Cslib/Crypto/Protocols/PerfectSecrecy/Basic.lean +++ b/Cslib/Crypto/Protocols/PerfectSecrecy/Basic.lean @@ -6,7 +6,6 @@ Authors: Samuel Schlesinger module -public import Cslib.Crypto.Protocols.PerfectSecrecy.Defs public import Cslib.Crypto.Protocols.PerfectSecrecy.Internal.PerfectSecrecy /-! diff --git a/Cslib/Crypto/Protocols/PerfectSecrecy/Defs.lean b/Cslib/Crypto/Protocols/PerfectSecrecy/Defs.lean index e7d824dd6..38c03b2ec 100644 --- a/Cslib/Crypto/Protocols/PerfectSecrecy/Defs.lean +++ b/Cslib/Crypto/Protocols/PerfectSecrecy/Defs.lean @@ -8,7 +8,6 @@ module public import Cslib.Crypto.Protocols.PerfectSecrecy.Encryption public import Cslib.Probability.PMF -public import Mathlib.Probability.ProbabilityMassFunction.Constructions /-! # Perfect Secrecy: Definitions diff --git a/Cslib/Crypto/Protocols/PerfectSecrecy/Internal/PerfectSecrecy.lean b/Cslib/Crypto/Protocols/PerfectSecrecy/Internal/PerfectSecrecy.lean index 66656e8ba..310dfc4d7 100644 --- a/Cslib/Crypto/Protocols/PerfectSecrecy/Internal/PerfectSecrecy.lean +++ b/Cslib/Crypto/Protocols/PerfectSecrecy/Internal/PerfectSecrecy.lean @@ -7,7 +7,6 @@ Authors: Samuel Schlesinger module public import Cslib.Crypto.Protocols.PerfectSecrecy.Defs -public import Mathlib.Probability.Distributions.Uniform /-! # Perfect Secrecy: Internal proofs diff --git a/Cslib/Crypto/Protocols/PerfectSecrecy/OneTimePad.lean b/Cslib/Crypto/Protocols/PerfectSecrecy/OneTimePad.lean index ed53950f6..320d67800 100644 --- a/Cslib/Crypto/Protocols/PerfectSecrecy/OneTimePad.lean +++ b/Cslib/Crypto/Protocols/PerfectSecrecy/OneTimePad.lean @@ -8,7 +8,6 @@ module public import Cslib.Crypto.Protocols.PerfectSecrecy.Basic public import Cslib.Crypto.Protocols.PerfectSecrecy.Internal.OneTimePad -public import Mathlib.Probability.Distributions.Uniform /-! # One-Time Pad diff --git a/Cslib/Crypto/Protocols/SecretSharing/Defs.lean b/Cslib/Crypto/Protocols/SecretSharing/Defs.lean index e8788f08d..d9d278b8f 100644 --- a/Cslib/Crypto/Protocols/SecretSharing/Defs.lean +++ b/Cslib/Crypto/Protocols/SecretSharing/Defs.lean @@ -6,8 +6,8 @@ Authors: Samuel Schlesinger module -public import Cslib.Probability.PMF public import Cslib.Crypto.Protocols.SecretSharing.Scheme +public import Cslib.Probability.PMF /-! # Secret Sharing: Definitions diff --git a/Cslib/Crypto/Protocols/SecretSharing/Scheme.lean b/Cslib/Crypto/Protocols/SecretSharing/Scheme.lean index 09e07ae2a..d1bdde4ea 100644 --- a/Cslib/Crypto/Protocols/SecretSharing/Scheme.lean +++ b/Cslib/Crypto/Protocols/SecretSharing/Scheme.lean @@ -7,7 +7,6 @@ Authors: Samuel Schlesinger module public import Cslib.Init -public import Mathlib.Data.Finset.Basic public import Mathlib.Probability.ProbabilityMassFunction.Constructions /-! diff --git a/Cslib/Crypto/Protocols/SecretSharing/Shamir.lean b/Cslib/Crypto/Protocols/SecretSharing/Shamir.lean index bd0de00d3..b5845038b 100644 --- a/Cslib/Crypto/Protocols/SecretSharing/Shamir.lean +++ b/Cslib/Crypto/Protocols/SecretSharing/Shamir.lean @@ -7,8 +7,9 @@ Authors: Samuel Schlesinger module public import Cslib.Crypto.Protocols.SecretSharing.Scheme -public import Mathlib.Probability.Distributions.Uniform public import Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial +public import Mathlib.Probability.Distributions.Uniform + import Cslib.Probability.PMF /-! diff --git a/Cslib/Foundations/Combinatorics/InfiniteGraphRamsey.lean b/Cslib/Foundations/Combinatorics/InfiniteGraphRamsey.lean index 17f1bb30f..6fa6501e7 100644 --- a/Cslib/Foundations/Combinatorics/InfiniteGraphRamsey.lean +++ b/Cslib/Foundations/Combinatorics/InfiniteGraphRamsey.lean @@ -7,7 +7,6 @@ Authors: Ching-Tsun Chou module public import Cslib.Init -public import Mathlib.Algebra.Order.Group.Nat public import Mathlib.Data.Fintype.Pigeonhole public import Mathlib.Data.Set.Finite.Basic public import Mathlib.Data.Set.Lattice diff --git a/Cslib/Foundations/Data/BiTape.lean b/Cslib/Foundations/Data/BiTape.lean index 8c57a4c11..879e07c9d 100644 --- a/Cslib/Foundations/Data/BiTape.lean +++ b/Cslib/Foundations/Data/BiTape.lean @@ -8,9 +8,6 @@ module public import Cslib.Foundations.Data.StackTape public import Mathlib.Computability.TuringMachine.Tape -public import Mathlib.Data.Finset.Attr -public import Mathlib.Tactic.SetLike -public import Mathlib.Algebra.Order.Group.Nat /-! # BiTape: Bidirectionally infinite TM tape representation using StackTape diff --git a/Cslib/Foundations/Data/FinFun/Update.lean b/Cslib/Foundations/Data/FinFun/Update.lean index d02941e77..220026b30 100644 --- a/Cslib/Foundations/Data/FinFun/Update.lean +++ b/Cslib/Foundations/Data/FinFun/Update.lean @@ -6,8 +6,8 @@ Authors: Fabrizio Montesi module -public import Cslib.Foundations.Data.FinFun.Basic public import Cslib.Foundations.Data.DecidableEqZero +public import Cslib.Foundations.Data.FinFun.Basic public import Mathlib.Data.Finset.SDiff /-! # Update for finite functions diff --git a/Cslib/Foundations/Data/HasFresh.lean b/Cslib/Foundations/Data/HasFresh.lean index df3d980e0..49b7a4867 100644 --- a/Cslib/Foundations/Data/HasFresh.lean +++ b/Cslib/Foundations/Data/HasFresh.lean @@ -8,8 +8,8 @@ module -- shake: keep-downstream public import Cslib.Init public import Mathlib.Analysis.Normed.Field.Lemmas + meta import Lean.Elab.ConfigEval -import Qq /-! Computable chacterization of infinite types. -/ diff --git a/Cslib/Foundations/Data/Nat/Segment.lean b/Cslib/Foundations/Data/Nat/Segment.lean index 01ec8fae8..236bb68ba 100644 --- a/Cslib/Foundations/Data/Nat/Segment.lean +++ b/Cslib/Foundations/Data/Nat/Segment.lean @@ -7,7 +7,6 @@ Authors: Ching-Tsun Chou module public import Cslib.Init -public import Mathlib.Algebra.Order.Sub.Basic public import Mathlib.Data.Nat.Nth /-! diff --git a/Cslib/Foundations/Data/OmegaSequence/Init.lean b/Cslib/Foundations/Data/OmegaSequence/Init.lean index 0013a221a..b91de65f4 100644 --- a/Cslib/Foundations/Data/OmegaSequence/Init.lean +++ b/Cslib/Foundations/Data/OmegaSequence/Init.lean @@ -8,7 +8,6 @@ module public import Cslib.Foundations.Data.OmegaSequence.Defs public import Mathlib.Algebra.Order.Group.Nat -public import Mathlib.Algebra.Order.Sub.Basic public import Mathlib.Order.Lattice.Nat /-! diff --git a/Cslib/Foundations/Data/Set/Saturation.lean b/Cslib/Foundations/Data/Set/Saturation.lean index 32e9806db..395d8c8e6 100644 --- a/Cslib/Foundations/Data/Set/Saturation.lean +++ b/Cslib/Foundations/Data/Set/Saturation.lean @@ -7,8 +7,8 @@ Authors: Ching-Tsun Chou module public import Cslib.Init -public import Mathlib.Order.SetNotation public import Mathlib.Data.Set.Basic +public import Mathlib.Order.SetNotation /-! # Saturation diff --git a/Cslib/Foundations/Logic/LogicalEquivalence.lean b/Cslib/Foundations/Logic/LogicalEquivalence.lean index 7f6c0d332..ddfacf47f 100644 --- a/Cslib/Foundations/Logic/LogicalEquivalence.lean +++ b/Cslib/Foundations/Logic/LogicalEquivalence.lean @@ -6,7 +6,6 @@ Authors: Fabrizio Montesi module -public import Cslib.Foundations.Syntax.Context public import Cslib.Foundations.Syntax.Congruence /-! Typeclass and notation for logical equivalence. -/ diff --git a/Cslib/Foundations/Relation/Attr.lean b/Cslib/Foundations/Relation/Attr.lean index 0b2d03778..49ad243d5 100644 --- a/Cslib/Foundations/Relation/Attr.lean +++ b/Cslib/Foundations/Relation/Attr.lean @@ -7,9 +7,8 @@ Authors: Fabrizio Montesi, Thomas Waring, Chris Henson module public import Cslib.Init -public import Lean.Elab.Command -public import Mathlib.Util.Notation3 public import Mathlib.Logic.Relation +public import Mathlib.Util.Notation3 /-! # Relations: Attributes diff --git a/Cslib/Foundations/Relation/Defs.lean b/Cslib/Foundations/Relation/Defs.lean index f649ed5dd..fdb4a7b95 100644 --- a/Cslib/Foundations/Relation/Defs.lean +++ b/Cslib/Foundations/Relation/Defs.lean @@ -9,7 +9,6 @@ module public import Cslib.Init public import Mathlib.Data.Set.CoeSort public import Mathlib.Logic.Relation -public import Mathlib.Order.Basic /-! # Relations: Definitions diff --git a/Cslib/Foundations/Relation/Restriction.lean b/Cslib/Foundations/Relation/Restriction.lean index 9de7da6d5..885005ff1 100644 --- a/Cslib/Foundations/Relation/Restriction.lean +++ b/Cslib/Foundations/Relation/Restriction.lean @@ -6,7 +6,6 @@ Authors: Chris Henson module -public import Cslib.Foundations.Relation.Defs public import Cslib.Foundations.Relation.Domain /-! # Relations: Properties on set restrictions diff --git a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean index d49a11a04..24177ca1f 100644 --- a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean @@ -7,7 +7,6 @@ Authors: Fabrizio Montesi, Thomas Waring module public import Cslib.Foundations.Relation.Domain -public import Cslib.Foundations.Semantics.LTS.Simulation public import Cslib.Foundations.Semantics.LTS.TraceEq public import Mathlib.Tactic.TFAE diff --git a/Cslib/Foundations/Semantics/LTS/LTSCat/Basic.lean b/Cslib/Foundations/Semantics/LTS/LTSCat/Basic.lean index d1e578db8..db6f92147 100644 --- a/Cslib/Foundations/Semantics/LTS/LTSCat/Basic.lean +++ b/Cslib/Foundations/Semantics/LTS/LTSCat/Basic.lean @@ -6,9 +6,8 @@ Authors: Ayberk Tosun module -public import Mathlib.CategoryTheory.Category.Basic public import Cslib.Foundations.Semantics.LTS.Basic -public import Mathlib.Control.Basic +public import Mathlib.CategoryTheory.Category.Basic /-! # Category of Labelled Transition Systems diff --git a/Cslib/Foundations/Semantics/LTS/TraceEq.lean b/Cslib/Foundations/Semantics/LTS/TraceEq.lean index 45782b67a..6568c61aa 100644 --- a/Cslib/Foundations/Semantics/LTS/TraceEq.lean +++ b/Cslib/Foundations/Semantics/LTS/TraceEq.lean @@ -6,7 +6,6 @@ Authors: Fabrizio Montesi module -public import Cslib.Foundations.Semantics.LTS.Basic public import Cslib.Foundations.Semantics.LTS.Simulation /-! diff --git a/Cslib/Languages/CCS/Basic.lean b/Cslib/Languages/CCS/Basic.lean index c30c1849d..656b7dc9a 100644 --- a/Cslib/Languages/CCS/Basic.lean +++ b/Cslib/Languages/CCS/Basic.lean @@ -7,8 +7,6 @@ Authors: Fabrizio Montesi module public import Cslib.Foundations.Syntax.Context -public import Mathlib.Tactic.ToAdditive -public import Mathlib.Tactic.ToDual /-! # Calculus of Communicating Systems (CCS) diff --git a/Cslib/Languages/CCS/Semantics.lean b/Cslib/Languages/CCS/Semantics.lean index 7a5670fde..b4a113eae 100644 --- a/Cslib/Languages/CCS/Semantics.lean +++ b/Cslib/Languages/CCS/Semantics.lean @@ -6,8 +6,8 @@ Authors: Fabrizio Montesi module -public import Cslib.Foundations.Semantics.LTS.HasTau public meta import Cslib.Foundations.Semantics.LTS.Notation +public import Cslib.Foundations.Semantics.LTS.HasTau public import Cslib.Languages.CCS.Basic /-! # Semantics of CCS diff --git a/Cslib/Languages/CombinatoryLogic/Basic.lean b/Cslib/Languages/CombinatoryLogic/Basic.lean index 785d4223d..5c11d2925 100644 --- a/Cslib/Languages/CombinatoryLogic/Basic.lean +++ b/Cslib/Languages/CombinatoryLogic/Basic.lean @@ -7,6 +7,7 @@ Authors: Thomas Waring module public import Cslib.Languages.CombinatoryLogic.Defs +public import Mathlib.Tactic.SplitIfs /-! # Basic results for the SKI calculus diff --git a/Cslib/Languages/CombinatoryLogic/Confluence.lean b/Cslib/Languages/CombinatoryLogic/Confluence.lean index 9fc3c7d18..414a83e98 100644 --- a/Cslib/Languages/CombinatoryLogic/Confluence.lean +++ b/Cslib/Languages/CombinatoryLogic/Confluence.lean @@ -6,8 +6,8 @@ Authors: Thomas Waring module -public import Cslib.Languages.CombinatoryLogic.Defs public import Cslib.Foundations.Relation.Confluence +public import Cslib.Languages.CombinatoryLogic.Defs /-! # SKI reduction is confluent diff --git a/Cslib/Languages/CombinatoryLogic/Defs.lean b/Cslib/Languages/CombinatoryLogic/Defs.lean index 7d028d283..df76218fd 100644 --- a/Cslib/Languages/CombinatoryLogic/Defs.lean +++ b/Cslib/Languages/CombinatoryLogic/Defs.lean @@ -6,9 +6,9 @@ Authors: Thomas Waring module +public meta import Mathlib.Tactic.ToDual public import Cslib.Foundations.Relation.Attr public import Cslib.Foundations.Relation.Defs -public meta import Mathlib.Tactic.ToDual /-! # SKI Combinatory Logic diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Safety.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Safety.lean index 609e129a6..9878bb96e 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Safety.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Safety.lean @@ -6,9 +6,9 @@ Authors: Chris Henson module +public import Cslib.Foundations.Relation.Confluence public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta -public import Cslib.Foundations.Relation.Confluence /-! # λ-calculus diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean index cb858529d..032703861 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean @@ -6,12 +6,8 @@ Authors: David Wegmann module -public import Cslib.Foundations.Data.HasFresh -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm /-! Strong normalization (termination) for full beta-reduction of simply typed lambda calculus. -/ diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean index a2be62e5a..1cff47bad 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean @@ -7,7 +7,6 @@ Authors: Maximiliano Onofre Martínez module public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties /-! # Call-by-Name Evaluation -/ diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean index bb064d21d..65595658c 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean @@ -7,7 +7,6 @@ Authors: Chris Henson module public import Cslib.Foundations.Relation.Attr -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Congruence /-! # β-reduction for the λ-calculus diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean index 2f1f00360..d75752d6e 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean @@ -6,8 +6,8 @@ Authors: Chris Henson module -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta public import Cslib.Foundations.Relation.Confluence +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta /-! # β-confluence for the λ-calculus -/ diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEtaConfluence.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEtaConfluence.lean index 2412f2c10..c0b0cf3b8 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEtaConfluence.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEtaConfluence.lean @@ -6,8 +6,6 @@ Authors: Maximiliano Onofre Martínez module -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEtaConfluence public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaEta /-! # βη-Confluence for the λ-calculus diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean index 2231d2b08..b9edc0551 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean @@ -7,7 +7,6 @@ Authors: Maximiliano Onofre Martínez module public import Cslib.Foundations.Relation.Attr -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Congruence /-! # η-reduction for the λ-calculus -/ diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEtaConfluence.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEtaConfluence.lean index 4defb563e..f97dad2d8 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEtaConfluence.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEtaConfluence.lean @@ -6,8 +6,8 @@ Authors: Maximiliano Onofre Martínez module -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEta public import Cslib.Foundations.Relation.Confluence +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEta /-! # η-confluence for the λ-calculus diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean index 91deb0e11..995cb31a7 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean @@ -7,10 +7,7 @@ Authors: David Wegmann module -public import Cslib.Foundations.Data.HasFresh -public import Cslib.Foundations.Syntax.HasSubstitution public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta /-! Multiple substitution for untyped lambda calculus. -/ diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean index ea45ee0e8..89f798460 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean @@ -6,10 +6,8 @@ Authors: David Wegmann module -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiApp -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt public import Cslib.Foundations.Relation.Confluence +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiApp /-! Strong normalization (termination) for full beta-reduction of untyped lambda calculus. -/ diff --git a/Cslib/Logics/HML/LogicalEquivalence.lean b/Cslib/Logics/HML/LogicalEquivalence.lean index 5bad96e46..2391de9b1 100644 --- a/Cslib/Logics/HML/LogicalEquivalence.lean +++ b/Cslib/Logics/HML/LogicalEquivalence.lean @@ -6,8 +6,8 @@ Authors: Fabrizio Montesi module -public import Cslib.Logics.HML.Basic public import Cslib.Foundations.Logic.LogicalEquivalence +public import Cslib.Logics.HML.Basic /-! # Logical Equivalence in HML diff --git a/Cslib/Logics/LinearLogic/CLL/Basic.lean b/Cslib/Logics/LinearLogic/CLL/Basic.lean index c331ae2ae..a208b5e3c 100644 --- a/Cslib/Logics/LinearLogic/CLL/Basic.lean +++ b/Cslib/Logics/LinearLogic/CLL/Basic.lean @@ -6,8 +6,6 @@ Authors: Fabrizio Montesi module -public import Cslib.Init -public import Cslib.Foundations.Syntax.Context public import Cslib.Foundations.Logic.InferenceSystem public import Cslib.Foundations.Logic.LogicalEquivalence public import Mathlib.Data.Multiset.Fold diff --git a/Cslib/Logics/LinearLogic/CLL/MLL.lean b/Cslib/Logics/LinearLogic/CLL/MLL.lean index 0e3c39354..4f56285af 100644 --- a/Cslib/Logics/LinearLogic/CLL/MLL.lean +++ b/Cslib/Logics/LinearLogic/CLL/MLL.lean @@ -7,7 +7,6 @@ Authors: Fabrizio Montesi module public import Cslib.Logics.LinearLogic.CLL.Basic -public import Cslib.Foundations.Logic.InferenceSystem /-! # Multiplicative Classical Linear Logic (MLL) diff --git a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean index fbb2fe840..9298488c0 100644 --- a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean +++ b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean @@ -6,10 +6,10 @@ Authors: Tanner Duve, Bhavik Mehta module -public import Mathlib.Algebra.Group.Pointwise.Set.Basic +public import Cslib.Logics.LinearLogic.CLL.Basic public import Mathlib.Algebra.Group.Idempotent +public import Mathlib.Algebra.Group.Pointwise.Set.Basic public import Mathlib.Order.Closure -public import Cslib.Logics.LinearLogic.CLL.Basic /-! # Phase semantics for Classical Linear Logic diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean index fda217a1c..51bfb4b3f 100644 --- a/Cslib/Logics/Modal/Basic.lean +++ b/Cslib/Logics/Modal/Basic.lean @@ -6,12 +6,8 @@ Authors: Fabrizio Montesi, Marianna Girlando module -public import Cslib.Init public import Cslib.Foundations.Logic.InferenceSystem -public import Mathlib.Data.Set.Basic -public import Mathlib.Order.Defs.Unbundled public import Cslib.Foundations.Relation.Euclidean -public import Mathlib.Logic.Nonempty /-! # Modal Logic diff --git a/Cslib/Logics/Modal/LogicalEquivalence.lean b/Cslib/Logics/Modal/LogicalEquivalence.lean index 0fc089e4e..1c4c2368c 100644 --- a/Cslib/Logics/Modal/LogicalEquivalence.lean +++ b/Cslib/Logics/Modal/LogicalEquivalence.lean @@ -6,8 +6,8 @@ Authors: Fabrizio Montesi module -public import Cslib.Logics.Modal.Basic public import Cslib.Foundations.Logic.LogicalEquivalence +public import Cslib.Logics.Modal.Basic /-! # Logical Equivalence in Modal Logic diff --git a/Cslib/Logics/Propositional/Defs.lean b/Cslib/Logics/Propositional/Defs.lean index e9c603d91..45d25ea68 100644 --- a/Cslib/Logics/Propositional/Defs.lean +++ b/Cslib/Logics/Propositional/Defs.lean @@ -7,8 +7,6 @@ Authors: Thomas Waring module public import Cslib.Foundations.Logic.InferenceSystem -public import Mathlib.Data.FunLike.Basic -public import Mathlib.Data.Set.Image public import Mathlib.Order.TypeTags /-! # Propositions and theories diff --git a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean index 560ecb69e..1fe01ead3 100644 --- a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean +++ b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean @@ -6,9 +6,6 @@ Authors: Thomas Waring module public import Cslib.Logics.Propositional.Defs -public import Cslib.Foundations.Logic.InferenceSystem -public import Mathlib.Data.Finset.Insert -public import Mathlib.Data.Finset.SDiff public import Mathlib.Data.Finset.Image /-! # Natural deduction for propositional logic diff --git a/Cslib/MachineLearning/PACLearning/Defs.lean b/Cslib/MachineLearning/PACLearning/Defs.lean index 084079f4b..6136db5b2 100644 --- a/Cslib/MachineLearning/PACLearning/Defs.lean +++ b/Cslib/MachineLearning/PACLearning/Defs.lean @@ -7,9 +7,7 @@ Authors: Samuel Schlesinger module public import Cslib.Init -public import Mathlib.MeasureTheory.Measure.MeasureSpace public import Mathlib.MeasureTheory.Constructions.Pi -public import Mathlib.Order.SymmDiff /-! # PAC Learning diff --git a/Cslib/MachineLearning/PACLearning/VersionSpace.lean b/Cslib/MachineLearning/PACLearning/VersionSpace.lean index 37f8072cf..209818a78 100644 --- a/Cslib/MachineLearning/PACLearning/VersionSpace.lean +++ b/Cslib/MachineLearning/PACLearning/VersionSpace.lean @@ -7,8 +7,6 @@ Authors: Dhruv Gupta module public import Cslib.MachineLearning.PACLearning.Defs -public import Mathlib.MeasureTheory.Measure.Dirac -public import Mathlib.MeasureTheory.Measure.Map /-! # Version Space diff --git a/Cslib/Probability/PMF.lean b/Cslib/Probability/PMF.lean index 8393eb229..4afefba49 100644 --- a/Cslib/Probability/PMF.lean +++ b/Cslib/Probability/PMF.lean @@ -7,7 +7,6 @@ Authors: Samuel Schlesinger module public import Cslib.Init -public import Mathlib.Probability.ProbabilityMassFunction.Monad public import Mathlib.Probability.Distributions.Uniform /-! diff --git a/CslibTests/FreeMonad.lean b/CslibTests/FreeMonad.lean index 6e6ce0359..a073470ca 100644 --- a/CslibTests/FreeMonad.lean +++ b/CslibTests/FreeMonad.lean @@ -3,8 +3,6 @@ Copyright (c) 2025 Tanner Duve. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Tanner Duve -/ -import Cslib.Foundations.Control.Monad.Free -import Mathlib.Tactic.Cases import Cslib.Foundations.Control.Monad.Free.Fold import Cslib.Languages.LambdaCalculus.LocallyNameless.Context diff --git a/CslibTests/HML.lean b/CslibTests/HML.lean index 3e9346f2b..bdc13d02f 100644 --- a/CslibTests/HML.lean +++ b/CslibTests/HML.lean @@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Logics.HML.Basic import Cslib.Languages.CCS.Semantics +import Cslib.Logics.HML.Basic namespace CslibTests diff --git a/CslibTests/ImportWithMathlib.lean b/CslibTests/ImportWithMathlib.lean index c68f3b0ba..2f31c4b8f 100644 --- a/CslibTests/ImportWithMathlib.lean +++ b/CslibTests/ImportWithMathlib.lean @@ -1,2 +1,2 @@ -import Mathlib import Cslib +import Mathlib diff --git a/CslibTests/LTS.lean b/CslibTests/LTS.lean index 34f3c3db9..ac9870e69 100644 --- a/CslibTests/LTS.lean +++ b/CslibTests/LTS.lean @@ -4,10 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Foundations.Semantics.LTS.Divergence import Cslib.Foundations.Semantics.LTS.Bisimulation -import Mathlib.Algebra.Group.Even -import Mathlib.Algebra.Ring.Parity +import Cslib.Foundations.Semantics.LTS.Divergence import Cslib.Foundations.Semantics.LTS.Notation namespace CslibTests diff --git a/CslibTests/Reduction.lean b/CslibTests/Reduction.lean index fdd55a97a..41d3f5010 100644 --- a/CslibTests/Reduction.lean +++ b/CslibTests/Reduction.lean @@ -1,4 +1,5 @@ import Cslib.Foundations.Relation.Attr +import Cslib.Init namespace CslibTests diff --git a/scripts/CheckInitImports.lean b/scripts/CheckInitImports.lean index e3aca2ad4..13bea84b3 100644 --- a/scripts/CheckInitImports.lean +++ b/scripts/CheckInitImports.lean @@ -4,10 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jesse Alama, Chris Henson -/ -import Lean -import Mathlib.Lean.CoreM import Batteries.Data.List.Basic -import ImportGraph +import Mathlib.Lean.CoreM open Lean Core Elab Command