From 15e9b1daa0b76f57a21c4b53bc793789bf71d2fd Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Sat, 3 Jan 2026 11:05:48 -0600 Subject: [PATCH 1/5] feat: move to the module system --- Cslib.lean | 154 +++++++++--------- .../Algorithms/Lean/MergeSort/MergeSort.lean | 11 +- Cslib/Algorithms/Lean/TimeM.lean | 4 + .../Automata/Acceptors/Acceptor.lean | 8 +- .../Automata/Acceptors/OmegaAcceptor.lean | 6 +- Cslib/Computability/Automata/DA/Basic.lean | 12 +- Cslib/Computability/Automata/DA/Buchi.lean | 6 +- Cslib/Computability/Automata/DA/Prod.lean | 8 +- Cslib/Computability/Automata/DA/ToNA.lean | 10 +- .../Automata/EpsilonNA/Basic.lean | 8 +- .../Automata/EpsilonNA/ToNA.lean | 8 +- Cslib/Computability/Automata/NA/Basic.lean | 12 +- .../Computability/Automata/NA/BuchiEquiv.lean | 6 +- .../Computability/Automata/NA/BuchiInter.lean | 10 +- Cslib/Computability/Automata/NA/Concat.lean | 8 +- Cslib/Computability/Automata/NA/Hist.lean | 6 +- Cslib/Computability/Automata/NA/Prod.lean | 6 +- Cslib/Computability/Automata/NA/Sum.lean | 6 +- Cslib/Computability/Automata/NA/ToDA.lean | 10 +- .../Languages/ExampleEventuallyZero.lean | 6 +- Cslib/Computability/Languages/Language.lean | 8 +- .../Languages/OmegaLanguage.lean | 12 +- .../Languages/OmegaRegularLanguage.lean | 22 ++- .../Languages/RegularLanguage.lean | 16 +- Cslib/Foundations/Control/Monad/Free.lean | 5 + .../Control/Monad/Free/Effects.lean | 9 +- .../Foundations/Control/Monad/Free/Fold.lean | 7 +- Cslib/Foundations/Data/FinFun.lean | 12 +- Cslib/Foundations/Data/HasFresh.lean | 12 +- Cslib/Foundations/Data/Nat/Segment.lean | 10 +- .../Foundations/Data/OmegaSequence/Defs.lean | 10 +- .../Data/OmegaSequence/Flatten.lean | 8 +- .../Data/OmegaSequence/InfOcc.lean | 10 +- .../Foundations/Data/OmegaSequence/Init.lean | 12 +- .../Data/OmegaSequence/Temporal.lean | 8 +- Cslib/Foundations/Data/Relation.lean | 14 +- Cslib/Foundations/Lint/Basic.lean | 8 +- Cslib/Foundations/Semantics/FLTS/Basic.lean | 6 +- .../Foundations/Semantics/FLTS/FLTSToLTS.lean | 8 +- .../Foundations/Semantics/FLTS/LTSToFLTS.lean | 8 +- Cslib/Foundations/Semantics/FLTS/Prod.lean | 6 +- Cslib/Foundations/Semantics/LTS/Basic.lean | 16 +- .../Semantics/LTS/Bisimulation.lean | 10 +- .../Foundations/Semantics/LTS/Simulation.lean | 6 +- Cslib/Foundations/Semantics/LTS/TraceEq.lean | 6 +- .../Semantics/ReductionSystem/Basic.lean | 10 +- Cslib/Foundations/Syntax/HasAlphaEquiv.lean | 6 +- Cslib/Foundations/Syntax/HasSubstitution.lean | 6 +- Cslib/Foundations/Syntax/HasWellFormed.lean | 6 +- Cslib/Init.lean | 8 +- Cslib/Languages/CCS/Basic.lean | 6 +- Cslib/Languages/CCS/BehaviouralTheory.lean | 8 +- Cslib/Languages/CCS/Semantics.lean | 8 +- Cslib/Languages/CombinatoryLogic/Basic.lean | 7 +- .../CombinatoryLogic/Confluence.lean | 8 +- Cslib/Languages/CombinatoryLogic/Defs.lean | 6 +- .../CombinatoryLogic/Evaluation.lean | 8 +- .../Languages/CombinatoryLogic/Recursion.lean | 6 +- .../LocallyNameless/Context.lean | 10 +- .../LocallyNameless/Fsub/Basic.lean | 8 +- .../LocallyNameless/Fsub/Opening.lean | 8 +- .../LocallyNameless/Fsub/Reduction.lean | 10 +- .../LocallyNameless/Fsub/Safety.lean | 6 +- .../LocallyNameless/Fsub/Subtype.lean | 6 +- .../LocallyNameless/Fsub/Typing.lean | 8 +- .../LocallyNameless/Fsub/WellFormed.lean | 6 +- .../LocallyNameless/Stlc/Basic.lean | 8 +- .../LocallyNameless/Stlc/Safety.lean | 10 +- .../LocallyNameless/Untyped/Basic.lean | 8 +- .../LocallyNameless/Untyped/FullBeta.lean | 10 +- .../Untyped/FullBetaConfluence.lean | 8 +- .../LocallyNameless/Untyped/Properties.lean | 6 +- .../LambdaCalculus/Named/Untyped/Basic.lean | 10 +- Cslib/Logics/LinearLogic/CLL/Basic.lean | 16 +- .../LinearLogic/CLL/CutElimination.lean | 6 +- .../Logics/LinearLogic/CLL/EtaExpansion.lean | 6 +- .../LinearLogic/CLL/PhaseSemantics/Basic.lean | 17 +- 77 files changed, 564 insertions(+), 250 deletions(-) diff --git a/Cslib.lean b/Cslib.lean index 249bd723..68be86a1 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -1,76 +1,78 @@ -import Cslib.Algorithms.Lean.MergeSort.MergeSort -import Cslib.Algorithms.Lean.TimeM -import Cslib.Computability.Automata.Acceptors.Acceptor -import Cslib.Computability.Automata.Acceptors.OmegaAcceptor -import Cslib.Computability.Automata.DA.Basic -import Cslib.Computability.Automata.DA.Buchi -import Cslib.Computability.Automata.DA.Prod -import Cslib.Computability.Automata.DA.ToNA -import Cslib.Computability.Automata.EpsilonNA.Basic -import Cslib.Computability.Automata.EpsilonNA.ToNA -import Cslib.Computability.Automata.NA.Basic -import Cslib.Computability.Automata.NA.BuchiEquiv -import Cslib.Computability.Automata.NA.BuchiInter -import Cslib.Computability.Automata.NA.Concat -import Cslib.Computability.Automata.NA.Hist -import Cslib.Computability.Automata.NA.Prod -import Cslib.Computability.Automata.NA.Sum -import Cslib.Computability.Automata.NA.ToDA -import Cslib.Computability.Languages.ExampleEventuallyZero -import Cslib.Computability.Languages.Language -import Cslib.Computability.Languages.OmegaLanguage -import Cslib.Computability.Languages.OmegaRegularLanguage -import Cslib.Computability.Languages.RegularLanguage -import Cslib.Foundations.Control.Monad.Free -import Cslib.Foundations.Control.Monad.Free.Effects -import Cslib.Foundations.Control.Monad.Free.Fold -import Cslib.Foundations.Data.FinFun -import Cslib.Foundations.Data.HasFresh -import Cslib.Foundations.Data.Nat.Segment -import Cslib.Foundations.Data.OmegaSequence.Defs -import Cslib.Foundations.Data.OmegaSequence.Flatten -import Cslib.Foundations.Data.OmegaSequence.InfOcc -import Cslib.Foundations.Data.OmegaSequence.Init -import Cslib.Foundations.Data.OmegaSequence.Temporal -import Cslib.Foundations.Data.Relation -import Cslib.Foundations.Lint.Basic -import Cslib.Foundations.Semantics.FLTS.Basic -import Cslib.Foundations.Semantics.FLTS.FLTSToLTS -import Cslib.Foundations.Semantics.FLTS.LTSToFLTS -import Cslib.Foundations.Semantics.FLTS.Prod -import Cslib.Foundations.Semantics.LTS.Basic -import Cslib.Foundations.Semantics.LTS.Bisimulation -import Cslib.Foundations.Semantics.LTS.Simulation -import Cslib.Foundations.Semantics.LTS.TraceEq -import Cslib.Foundations.Semantics.ReductionSystem.Basic -import Cslib.Foundations.Syntax.HasAlphaEquiv -import Cslib.Foundations.Syntax.HasSubstitution -import Cslib.Foundations.Syntax.HasWellFormed -import Cslib.Init -import Cslib.Languages.CCS.Basic -import Cslib.Languages.CCS.BehaviouralTheory -import Cslib.Languages.CCS.Semantics -import Cslib.Languages.CombinatoryLogic.Basic -import Cslib.Languages.CombinatoryLogic.Confluence -import Cslib.Languages.CombinatoryLogic.Defs -import Cslib.Languages.CombinatoryLogic.Evaluation -import Cslib.Languages.CombinatoryLogic.Recursion -import Cslib.Languages.LambdaCalculus.LocallyNameless.Context -import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Basic -import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Opening -import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Reduction -import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Safety -import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Subtype -import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Typing -import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.WellFormed -import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic -import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Safety -import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic -import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta -import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence -import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties -import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic -import Cslib.Logics.LinearLogic.CLL.Basic -import Cslib.Logics.LinearLogic.CLL.CutElimination -import Cslib.Logics.LinearLogic.CLL.EtaExpansion -import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic +module + +public import Cslib.Algorithms.Lean.MergeSort.MergeSort +public import Cslib.Algorithms.Lean.TimeM +public import Cslib.Computability.Automata.Acceptors.Acceptor +public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor +public import Cslib.Computability.Automata.DA.Basic +public import Cslib.Computability.Automata.DA.Buchi +public import Cslib.Computability.Automata.DA.Prod +public import Cslib.Computability.Automata.DA.ToNA +public import Cslib.Computability.Automata.EpsilonNA.Basic +public import Cslib.Computability.Automata.EpsilonNA.ToNA +public import Cslib.Computability.Automata.NA.Basic +public import Cslib.Computability.Automata.NA.BuchiEquiv +public import Cslib.Computability.Automata.NA.BuchiInter +public import Cslib.Computability.Automata.NA.Concat +public import Cslib.Computability.Automata.NA.Hist +public import Cslib.Computability.Automata.NA.Prod +public import Cslib.Computability.Automata.NA.Sum +public import Cslib.Computability.Automata.NA.ToDA +public import Cslib.Computability.Languages.ExampleEventuallyZero +public import Cslib.Computability.Languages.Language +public import Cslib.Computability.Languages.OmegaLanguage +public import Cslib.Computability.Languages.OmegaRegularLanguage +public import Cslib.Computability.Languages.RegularLanguage +public import Cslib.Foundations.Control.Monad.Free +public import Cslib.Foundations.Control.Monad.Free.Effects +public import Cslib.Foundations.Control.Monad.Free.Fold +public import Cslib.Foundations.Data.FinFun +public import Cslib.Foundations.Data.HasFresh +public import Cslib.Foundations.Data.Nat.Segment +public import Cslib.Foundations.Data.OmegaSequence.Defs +public import Cslib.Foundations.Data.OmegaSequence.Flatten +public import Cslib.Foundations.Data.OmegaSequence.InfOcc +public import Cslib.Foundations.Data.OmegaSequence.Init +public import Cslib.Foundations.Data.OmegaSequence.Temporal +public import Cslib.Foundations.Data.Relation +public import Cslib.Foundations.Lint.Basic +public import Cslib.Foundations.Semantics.FLTS.Basic +public import Cslib.Foundations.Semantics.FLTS.FLTSToLTS +public import Cslib.Foundations.Semantics.FLTS.LTSToFLTS +public import Cslib.Foundations.Semantics.FLTS.Prod +public import Cslib.Foundations.Semantics.LTS.Basic +public import Cslib.Foundations.Semantics.LTS.Bisimulation +public import Cslib.Foundations.Semantics.LTS.Simulation +public import Cslib.Foundations.Semantics.LTS.TraceEq +public import Cslib.Foundations.Semantics.ReductionSystem.Basic +public import Cslib.Foundations.Syntax.HasAlphaEquiv +public import Cslib.Foundations.Syntax.HasSubstitution +public import Cslib.Foundations.Syntax.HasWellFormed +public import Cslib.Init +public import Cslib.Languages.CCS.Basic +public import Cslib.Languages.CCS.BehaviouralTheory +public import Cslib.Languages.CCS.Semantics +public import Cslib.Languages.CombinatoryLogic.Basic +public import Cslib.Languages.CombinatoryLogic.Confluence +public import Cslib.Languages.CombinatoryLogic.Defs +public import Cslib.Languages.CombinatoryLogic.Evaluation +public import Cslib.Languages.CombinatoryLogic.Recursion +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Context +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Basic +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Opening +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Reduction +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Safety +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Subtype +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Typing +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.WellFormed +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Safety +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties +public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic +public import Cslib.Logics.LinearLogic.CLL.Basic +public import Cslib.Logics.LinearLogic.CLL.CutElimination +public import Cslib.Logics.LinearLogic.CLL.EtaExpansion +public import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic diff --git a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean index 6a474e73..c154a108 100644 --- a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean +++ b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean @@ -4,11 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Sorrachai Yingchareonthawornhcai -/ -import Cslib.Algorithms.Lean.TimeM -import Mathlib.Data.Nat.Cast.Order.Ring -import Mathlib.Data.Nat.Lattice -import Mathlib.Data.Nat.Log +module +public import Cslib.Algorithms.Lean.TimeM +public import Mathlib.Data.Nat.Cast.Order.Ring +public import Mathlib.Data.Nat.Lattice +public import Mathlib.Data.Nat.Log + +@[expose] public section /-! # MergeSort on a list diff --git a/Cslib/Algorithms/Lean/TimeM.lean b/Cslib/Algorithms/Lean/TimeM.lean index 1b46497b..ff7f0f73 100644 --- a/Cslib/Algorithms/Lean/TimeM.lean +++ b/Cslib/Algorithms/Lean/TimeM.lean @@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Sorrachai Yingchareonthawornhcai -/ +module + import Cslib.Init +@[expose] public section + /-! # TimeM: Time Complexity Monad diff --git a/Cslib/Computability/Automata/Acceptors/Acceptor.lean b/Cslib/Computability/Automata/Acceptors/Acceptor.lean index 2eba7f18..f3f98dc7 100644 --- a/Cslib/Computability/Automata/Acceptors/Acceptor.lean +++ b/Cslib/Computability/Automata/Acceptors/Acceptor.lean @@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Init -import Mathlib.Computability.Language +module + +public import Cslib.Init +public import Mathlib.Computability.Language + +@[expose] public section namespace Cslib.Automata diff --git a/Cslib/Computability/Automata/Acceptors/OmegaAcceptor.lean b/Cslib/Computability/Automata/Acceptors/OmegaAcceptor.lean index 7e6c402f..251b3b95 100644 --- a/Cslib/Computability/Automata/Acceptors/OmegaAcceptor.lean +++ b/Cslib/Computability/Automata/Acceptors/OmegaAcceptor.lean @@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Computability.Languages.OmegaLanguage +module + +public import Cslib.Computability.Languages.OmegaLanguage + +@[expose] public section namespace Cslib.Automata diff --git a/Cslib/Computability/Automata/DA/Basic.lean b/Cslib/Computability/Automata/DA/Basic.lean index 9c5c38f1..6914f8fc 100644 --- a/Cslib/Computability/Automata/DA/Basic.lean +++ b/Cslib/Computability/Automata/DA/Basic.lean @@ -4,10 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi, Ching-Tsun Chou -/ -import Cslib.Computability.Automata.Acceptors.Acceptor -import Cslib.Computability.Automata.Acceptors.OmegaAcceptor -import Cslib.Foundations.Data.OmegaSequence.InfOcc -import Cslib.Foundations.Semantics.FLTS.Basic +module + +public import Cslib.Computability.Automata.Acceptors.Acceptor +public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor +public import Cslib.Foundations.Data.OmegaSequence.InfOcc +public import Cslib.Foundations.Semantics.FLTS.Basic + +@[expose] public section /-! # Deterministic Automata diff --git a/Cslib/Computability/Automata/DA/Buchi.lean b/Cslib/Computability/Automata/DA/Buchi.lean index ea545274..ce4d4c66 100644 --- a/Cslib/Computability/Automata/DA/Buchi.lean +++ b/Cslib/Computability/Automata/DA/Buchi.lean @@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Ching-Tsun Chou -/ -import Cslib.Computability.Automata.DA.Basic +module + +public import Cslib.Computability.Automata.DA.Basic + +@[expose] public section /-! # Deterministic Buchi automata. -/ diff --git a/Cslib/Computability/Automata/DA/Prod.lean b/Cslib/Computability/Automata/DA/Prod.lean index a06d0e31..cf16fbd9 100644 --- a/Cslib/Computability/Automata/DA/Prod.lean +++ b/Cslib/Computability/Automata/DA/Prod.lean @@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Ching-Tsun Chou -/ -import Cslib.Computability.Automata.DA.Basic -import Cslib.Foundations.Semantics.FLTS.Prod +module + +public import Cslib.Computability.Automata.DA.Basic +public import Cslib.Foundations.Semantics.FLTS.Prod + +@[expose] public section /-! # Product of deterministic automata. -/ diff --git a/Cslib/Computability/Automata/DA/ToNA.lean b/Cslib/Computability/Automata/DA/ToNA.lean index 5d121189..dabbdc14 100644 --- a/Cslib/Computability/Automata/DA/ToNA.lean +++ b/Cslib/Computability/Automata/DA/ToNA.lean @@ -4,9 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Computability.Automata.DA.Basic -import Cslib.Computability.Automata.NA.Basic -import Cslib.Foundations.Semantics.FLTS.FLTSToLTS +module + +public import Cslib.Computability.Automata.DA.Basic +public import Cslib.Computability.Automata.NA.Basic +public import Cslib.Foundations.Semantics.FLTS.FLTSToLTS + +@[expose] public section /-! # Translation of Deterministic Automata into Nonodeterministic Automata. diff --git a/Cslib/Computability/Automata/EpsilonNA/Basic.lean b/Cslib/Computability/Automata/EpsilonNA/Basic.lean index 6083e1f3..ae2174f4 100644 --- a/Cslib/Computability/Automata/EpsilonNA/Basic.lean +++ b/Cslib/Computability/Automata/EpsilonNA/Basic.lean @@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi, Ching-Tsun Chou -/ -import Cslib.Computability.Automata.NA.Basic +module + +public import Cslib.Computability.Automata.NA.Basic + +@[expose] public section /-! # Nondeterministic automata with ε-transitions. -/ @@ -21,7 +25,7 @@ structure εNA (State Symbol : Type*) extends NA State (Option Symbol) variable {State Symbol : Type*} @[local grind =] -private instance : HasTau (Option α) := ⟨.none⟩ +instance : HasTau (Option α) := ⟨.none⟩ /-- The `ε`-closure of a set of states `S` is the set of states reachable by any state in `S` by performing only `ε`-transitions. We use `LTS.τClosure` since `ε` (`Option.none`) is an instance diff --git a/Cslib/Computability/Automata/EpsilonNA/ToNA.lean b/Cslib/Computability/Automata/EpsilonNA/ToNA.lean index 052a0cf8..4882cf65 100644 --- a/Cslib/Computability/Automata/EpsilonNA/ToNA.lean +++ b/Cslib/Computability/Automata/EpsilonNA/ToNA.lean @@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Computability.Automata.EpsilonNA.Basic +module + +public import Cslib.Computability.Automata.EpsilonNA.Basic + +@[expose] public section /-! # Translation of εNA into NA -/ @@ -13,7 +17,7 @@ namespace Cslib /-- Converts an `LTS` with Option labels into an `LTS` on the carried label type, by removing all ε-transitions. -/ @[local grind =] -private def LTS.noε (lts : LTS State (Option Label)) : LTS State Label where +def LTS.noε (lts : LTS State (Option Label)) : LTS State Label where Tr s μ s' := lts.Tr s (some μ) s' @[local grind .] diff --git a/Cslib/Computability/Automata/NA/Basic.lean b/Cslib/Computability/Automata/NA/Basic.lean index f7d88dc5..88ee3901 100644 --- a/Cslib/Computability/Automata/NA/Basic.lean +++ b/Cslib/Computability/Automata/NA/Basic.lean @@ -4,10 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi, Ching-Tsun Chou, Chris Henson. -/ -import Cslib.Computability.Automata.Acceptors.Acceptor -import Cslib.Computability.Automata.Acceptors.OmegaAcceptor -import Cslib.Foundations.Data.OmegaSequence.InfOcc -import Cslib.Foundations.Semantics.LTS.Basic +module + +public import Cslib.Computability.Automata.Acceptors.Acceptor +public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor +public import Cslib.Foundations.Data.OmegaSequence.InfOcc +public import Cslib.Foundations.Semantics.LTS.Basic + +@[expose] public section /-! # Nondeterministic Automaton diff --git a/Cslib/Computability/Automata/NA/BuchiEquiv.lean b/Cslib/Computability/Automata/NA/BuchiEquiv.lean index dd9c4b3c..3c065975 100644 --- a/Cslib/Computability/Automata/NA/BuchiEquiv.lean +++ b/Cslib/Computability/Automata/NA/BuchiEquiv.lean @@ -4,7 +4,11 @@ Relexsed under Apache 2.0 license xs described in the file LICENSE. Authors: Ching-Tsun Chou -/ -import Cslib.Computability.Automata.NA.Basic +module + +public import Cslib.Computability.Automata.NA.Basic + +@[expose] public section /-! # Equivalence of nondeterministic Buchi automata (NBAs). -/ diff --git a/Cslib/Computability/Automata/NA/BuchiInter.lean b/Cslib/Computability/Automata/NA/BuchiInter.lean index fad15c5f..8ac33b54 100644 --- a/Cslib/Computability/Automata/NA/BuchiInter.lean +++ b/Cslib/Computability/Automata/NA/BuchiInter.lean @@ -4,9 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Ching-Tsun Chou -/ -import Cslib.Computability.Automata.NA.Hist -import Cslib.Computability.Automata.NA.Prod -import Cslib.Foundations.Data.OmegaSequence.Temporal +module + +public import Cslib.Computability.Automata.NA.Hist +public import Cslib.Computability.Automata.NA.Prod +public import Cslib.Foundations.Data.OmegaSequence.Temporal + +@[expose] public section /-! # Intersection of nondeterministic Buchi automata. diff --git a/Cslib/Computability/Automata/NA/Concat.lean b/Cslib/Computability/Automata/NA/Concat.lean index 3a1b29d6..d306d28d 100644 --- a/Cslib/Computability/Automata/NA/Concat.lean +++ b/Cslib/Computability/Automata/NA/Concat.lean @@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Ching-Tsun Chou -/ -import Cslib.Computability.Automata.NA.Basic -import Cslib.Foundations.Data.OmegaSequence.Temporal +module + +public import Cslib.Computability.Automata.NA.Basic +public import Cslib.Foundations.Data.OmegaSequence.Temporal + +@[expose] public section /-! # Concatenation of nondeterministic automata. -/ diff --git a/Cslib/Computability/Automata/NA/Hist.lean b/Cslib/Computability/Automata/NA/Hist.lean index ec7dd0a2..004a1af2 100644 --- a/Cslib/Computability/Automata/NA/Hist.lean +++ b/Cslib/Computability/Automata/NA/Hist.lean @@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Ching-Tsun Chou -/ -import Cslib.Computability.Automata.NA.Basic +module + +public import Cslib.Computability.Automata.NA.Basic + +@[expose] public section /-! # Adding a history states to a nondeterministic automaton. diff --git a/Cslib/Computability/Automata/NA/Prod.lean b/Cslib/Computability/Automata/NA/Prod.lean index 9ed67298..9fb08c8b 100644 --- a/Cslib/Computability/Automata/NA/Prod.lean +++ b/Cslib/Computability/Automata/NA/Prod.lean @@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Ching-Tsun Chou -/ -import Cslib.Computability.Automata.NA.Basic +module + +public import Cslib.Computability.Automata.NA.Basic + +@[expose] public section /-! # Product of nondeterministic automata. -/ diff --git a/Cslib/Computability/Automata/NA/Sum.lean b/Cslib/Computability/Automata/NA/Sum.lean index 9ffd2ccf..12546435 100644 --- a/Cslib/Computability/Automata/NA/Sum.lean +++ b/Cslib/Computability/Automata/NA/Sum.lean @@ -4,7 +4,11 @@ Relexsed under Apache 2.0 license xs described in the file LICENSE. Authors: Ching-Tsun Chou -/ -import Cslib.Computability.Automata.NA.Basic +module + +public import Cslib.Computability.Automata.NA.Basic + +@[expose] public section /-! # Sum of nondeterministic automata. -/ diff --git a/Cslib/Computability/Automata/NA/ToDA.lean b/Cslib/Computability/Automata/NA/ToDA.lean index 6eda4a6b..041f6ab3 100644 --- a/Cslib/Computability/Automata/NA/ToDA.lean +++ b/Cslib/Computability/Automata/NA/ToDA.lean @@ -4,9 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Computability.Automata.DA.Basic -import Cslib.Computability.Automata.NA.Basic -import Cslib.Foundations.Semantics.FLTS.LTSToFLTS +module + +public import Cslib.Computability.Automata.DA.Basic +public import Cslib.Computability.Automata.NA.Basic +public import Cslib.Foundations.Semantics.FLTS.LTSToFLTS + +@[expose] public section /-! # Translation of Nondeterministic Automata for finite strings into Deterministic Automata diff --git a/Cslib/Computability/Languages/ExampleEventuallyZero.lean b/Cslib/Computability/Languages/ExampleEventuallyZero.lean index f786590e..6873af81 100644 --- a/Cslib/Computability/Languages/ExampleEventuallyZero.lean +++ b/Cslib/Computability/Languages/ExampleEventuallyZero.lean @@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Ching-Tsun Chou -/ -import Cslib.Computability.Automata.NA.Basic +module + +public import Cslib.Computability.Automata.NA.Basic + +@[expose] public section /-! # An ω-regular language that is not accepted by any deterministic Buchi automaton diff --git a/Cslib/Computability/Languages/Language.lean b/Cslib/Computability/Languages/Language.lean index 569171ed..2891329d 100644 --- a/Cslib/Computability/Languages/Language.lean +++ b/Cslib/Computability/Languages/Language.lean @@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Ching-Tsun Chou -/ -import Cslib.Init -import Mathlib.Computability.Language +module + +public import Cslib.Init +public import Mathlib.Computability.Language + +@[expose] public section /-! # Language (additional definitions and theorems) diff --git a/Cslib/Computability/Languages/OmegaLanguage.lean b/Cslib/Computability/Languages/OmegaLanguage.lean index 3765f654..679a0297 100644 --- a/Cslib/Computability/Languages/OmegaLanguage.lean +++ b/Cslib/Computability/Languages/OmegaLanguage.lean @@ -4,10 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Ching-Tsun Chou -/ -import Cslib.Computability.Languages.Language -import Cslib.Foundations.Data.OmegaSequence.Flatten -import Mathlib.Computability.Language -import Mathlib.Order.Filter.AtTopBot.Defs +module + +public import Cslib.Computability.Languages.Language +public import Cslib.Foundations.Data.OmegaSequence.Flatten +public import Mathlib.Computability.Language +public import Mathlib.Order.Filter.AtTopBot.Defs + +@[expose] public section /-! # ωLanguage diff --git a/Cslib/Computability/Languages/OmegaRegularLanguage.lean b/Cslib/Computability/Languages/OmegaRegularLanguage.lean index a32559ce..a3ad5dc7 100644 --- a/Cslib/Computability/Languages/OmegaRegularLanguage.lean +++ b/Cslib/Computability/Languages/OmegaRegularLanguage.lean @@ -4,15 +4,19 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Ching-Tsun Chou -/ -import Cslib.Computability.Automata.DA.Buchi -import Cslib.Computability.Automata.NA.BuchiEquiv -import Cslib.Computability.Automata.NA.BuchiInter -import Cslib.Computability.Automata.NA.Concat -import Cslib.Computability.Automata.NA.Sum -import Cslib.Computability.Languages.ExampleEventuallyZero -import Cslib.Computability.Languages.RegularLanguage -import Mathlib.Data.Finite.Sigma -import Mathlib.Data.Finite.Sum +module + +public import Cslib.Computability.Automata.DA.Buchi +public import Cslib.Computability.Automata.NA.BuchiEquiv +public import Cslib.Computability.Automata.NA.BuchiInter +public import Cslib.Computability.Automata.NA.Concat +public import Cslib.Computability.Automata.NA.Sum +public import Cslib.Computability.Languages.ExampleEventuallyZero +public import Cslib.Computability.Languages.RegularLanguage +public import Mathlib.Data.Finite.Sigma +public import Mathlib.Data.Finite.Sum + +@[expose] public section /-! # ω-Regular languages diff --git a/Cslib/Computability/Languages/RegularLanguage.lean b/Cslib/Computability/Languages/RegularLanguage.lean index c7d01175..a7aa145c 100644 --- a/Cslib/Computability/Languages/RegularLanguage.lean +++ b/Cslib/Computability/Languages/RegularLanguage.lean @@ -4,12 +4,16 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Ching-Tsun Chou -/ -import Cslib.Computability.Automata.DA.Prod -import Cslib.Computability.Automata.DA.ToNA -import Cslib.Computability.Automata.NA.ToDA -import Mathlib.Computability.DFA -import Mathlib.Data.Set.Card -import Mathlib.Tactic.Common +module + +public import Cslib.Computability.Automata.DA.Prod +public import Cslib.Computability.Automata.DA.ToNA +public import Cslib.Computability.Automata.NA.ToDA +public import Mathlib.Computability.DFA +public import Mathlib.Data.Set.Card +public import Mathlib.Tactic.Common + +@[expose] public section /-! # Regular languages diff --git a/Cslib/Foundations/Control/Monad/Free.lean b/Cslib/Foundations/Control/Monad/Free.lean index 14b486bb..9cf40c32 100644 --- a/Cslib/Foundations/Control/Monad/Free.lean +++ b/Cslib/Foundations/Control/Monad/Free.lean @@ -3,8 +3,13 @@ Copyright (c) 2025 Tanner Duve. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Tanner Duve, Eric Wieser -/ + +module + import Cslib.Init +@[expose] public section + /-! # Free Monad diff --git a/Cslib/Foundations/Control/Monad/Free/Effects.lean b/Cslib/Foundations/Control/Monad/Free/Effects.lean index 49a71f41..b8bc1311 100644 --- a/Cslib/Foundations/Control/Monad/Free/Effects.lean +++ b/Cslib/Foundations/Control/Monad/Free/Effects.lean @@ -3,8 +3,13 @@ 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.Control.Monad.Cont + +module + +public import Cslib.Foundations.Control.Monad.Free +public import Mathlib.Control.Monad.Cont + +@[expose] public section /-! # Free Monad diff --git a/Cslib/Foundations/Control/Monad/Free/Fold.lean b/Cslib/Foundations/Control/Monad/Free/Fold.lean index 223b8b1f..1bacac89 100644 --- a/Cslib/Foundations/Control/Monad/Free/Fold.lean +++ b/Cslib/Foundations/Control/Monad/Free/Fold.lean @@ -3,7 +3,12 @@ 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 + +module + +public import Cslib.Foundations.Control.Monad.Free + +@[expose] public section /-! # Free Monad Catamorphism diff --git a/Cslib/Foundations/Data/FinFun.lean b/Cslib/Foundations/Data/FinFun.lean index 23624f4c..3f5b54f9 100644 --- a/Cslib/Foundations/Data/FinFun.lean +++ b/Cslib/Foundations/Data/FinFun.lean @@ -4,9 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi, Xueying Qin -/ -import Cslib.Init -import Mathlib.Data.Finset.Filter -import Mathlib.Data.Finset.Lattice.Basic +module + +public import Cslib.Init +public import Mathlib.Data.Finset.Filter +public import Mathlib.Data.Finset.Lattice.Basic + +@[expose] public section /-! # Finite functions @@ -38,7 +42,7 @@ scoped infixr:25 " →₀ " => FinFun /-- Constructs a `FinFun` by restricting a function to a given support, filtering out all elements not mapped to 0 in the support. -/ @[scoped grind .] -private def fromFun {α β : Type*} [Zero β] [DecidableEq α] +def fromFun {α β : Type*} [Zero β] [DecidableEq α] [∀ y : β, Decidable (y = 0)] (fn : α → β) (support : Finset α) : α →₀ β where fn := (fun a => if a ∈ support then fn a else 0) support := support.filter (fn · ≠ 0) diff --git a/Cslib/Foundations/Data/HasFresh.lean b/Cslib/Foundations/Data/HasFresh.lean index 7a4a14cd..e9cb1e8e 100644 --- a/Cslib/Foundations/Data/HasFresh.lean +++ b/Cslib/Foundations/Data/HasFresh.lean @@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi, Kenny Lau -/ -import Cslib.Init -import Mathlib.Analysis.Normed.Field.Lemmas +module + +public import Cslib.Init +public import Mathlib.Analysis.Normed.Field.Lemmas + +@[expose] public section universe u @@ -26,6 +30,8 @@ in proofs. -/ theorem HasFresh.fresh_exists {α : Type u} [HasFresh α] (s : Finset α) : ∃ a, a ∉ s := ⟨fresh s, fresh_notMem s⟩ +public meta section + open Lean Elab Term Meta Parser Tactic /-- Configuration for the `free_union` term elaborator. -/ @@ -122,6 +128,8 @@ def HasFresh.freeUnion : TermElab := fun stx _ => do return union | _ => throwUnsupportedSyntax +end + export HasFresh (fresh fresh_notMem fresh_exists) lemma HasFresh.not_of_finite (α : Type u) [Fintype α] : IsEmpty (HasFresh α) := diff --git a/Cslib/Foundations/Data/Nat/Segment.lean b/Cslib/Foundations/Data/Nat/Segment.lean index 1906e549..b6b7a49d 100644 --- a/Cslib/Foundations/Data/Nat/Segment.lean +++ b/Cslib/Foundations/Data/Nat/Segment.lean @@ -4,9 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Ching-Tsun Chou -/ -import Cslib.Init -import Mathlib.Algebra.Order.Sub.Basic -import Mathlib.Data.Nat.Nth +module + +public import Cslib.Init +public import Mathlib.Algebra.Order.Sub.Basic +public import Mathlib.Data.Nat.Nth + +@[expose] public section open Function Set diff --git a/Cslib/Foundations/Data/OmegaSequence/Defs.lean b/Cslib/Foundations/Data/OmegaSequence/Defs.lean index 2e366cae..7146efc2 100644 --- a/Cslib/Foundations/Data/OmegaSequence/Defs.lean +++ b/Cslib/Foundations/Data/OmegaSequence/Defs.lean @@ -4,9 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Ching-Tsun Chou, Fabrizio Montesi -/ -import Cslib.Init -import Mathlib.Data.FunLike.Basic -import Mathlib.Logic.Function.Iterate +module + +public import Cslib.Init +public import Mathlib.Data.FunLike.Basic +public import Mathlib.Logic.Function.Iterate + +@[expose] public section /-! # Definition of `ωSequence` and functions on infinite sequences diff --git a/Cslib/Foundations/Data/OmegaSequence/Flatten.lean b/Cslib/Foundations/Data/OmegaSequence/Flatten.lean index 833d133b..6d171507 100644 --- a/Cslib/Foundations/Data/OmegaSequence/Flatten.lean +++ b/Cslib/Foundations/Data/OmegaSequence/Flatten.lean @@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Ching-Tsun Chou -/ -import Cslib.Foundations.Data.Nat.Segment -import Cslib.Foundations.Data.OmegaSequence.Init +module + +public import Cslib.Foundations.Data.Nat.Segment +public import Cslib.Foundations.Data.OmegaSequence.Init + +@[expose] public section /-! # Flattening an infinite sequence of lists diff --git a/Cslib/Foundations/Data/OmegaSequence/InfOcc.lean b/Cslib/Foundations/Data/OmegaSequence/InfOcc.lean index bec9333d..8dc76adf 100644 --- a/Cslib/Foundations/Data/OmegaSequence/InfOcc.lean +++ b/Cslib/Foundations/Data/OmegaSequence/InfOcc.lean @@ -4,9 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Ching-Tsun Chou -/ -import Cslib.Foundations.Data.OmegaSequence.Defs -import Mathlib.Order.Filter.AtTopBot.Basic -import Mathlib.Order.Filter.Cofinite +module + +public import Cslib.Foundations.Data.OmegaSequence.Defs +public import Mathlib.Order.Filter.AtTopBot.Basic +public import Mathlib.Order.Filter.Cofinite + +@[expose] public section /-! # Infinite occurrences diff --git a/Cslib/Foundations/Data/OmegaSequence/Init.lean b/Cslib/Foundations/Data/OmegaSequence/Init.lean index dc017d34..d5a8db79 100644 --- a/Cslib/Foundations/Data/OmegaSequence/Init.lean +++ b/Cslib/Foundations/Data/OmegaSequence/Init.lean @@ -4,10 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Ching-Tsun Chou, Fabrizio Montesi -/ -import Cslib.Foundations.Data.OmegaSequence.Defs -import Mathlib.Algebra.Order.Group.Nat -import Mathlib.Algebra.Order.Sub.Basic -import Mathlib.Data.Nat.Lattice +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.Data.Nat.Lattice + +@[expose] public section /-! # ω-sequences a.k.a. infinite sequences diff --git a/Cslib/Foundations/Data/OmegaSequence/Temporal.lean b/Cslib/Foundations/Data/OmegaSequence/Temporal.lean index 5bb432c9..3028acdb 100644 --- a/Cslib/Foundations/Data/OmegaSequence/Temporal.lean +++ b/Cslib/Foundations/Data/OmegaSequence/Temporal.lean @@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Ching-Tsun Chou -/ -import Cslib.Foundations.Data.OmegaSequence.Init -import Mathlib.Order.Filter.AtTopBot.Basic +module + +public import Cslib.Foundations.Data.OmegaSequence.Init +public import Mathlib.Order.Filter.AtTopBot.Basic + +@[expose] public section /-! # Temporal reasoning over infinite sequences. diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean index 7de93274..c6193e0b 100644 --- a/Cslib/Foundations/Data/Relation.lean +++ b/Cslib/Foundations/Data/Relation.lean @@ -4,11 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi, Thomas Waring, Chris Henson -/ -import Cslib.Init -import Mathlib.Logic.Relation -import Mathlib.Data.List.TFAE -import Mathlib.Order.WellFounded -import Mathlib.Order.BooleanAlgebra.Basic +module + +public import Cslib.Init +public import Mathlib.Logic.Relation +public import Mathlib.Data.List.TFAE +public import Mathlib.Order.WellFounded +public import Mathlib.Order.BooleanAlgebra.Basic + +@[expose] public section variable {α : Type*} {r : α → α → Prop} diff --git a/Cslib/Foundations/Lint/Basic.lean b/Cslib/Foundations/Lint/Basic.lean index b45bad2a..8a1fb2bc 100644 --- a/Cslib/Foundations/Lint/Basic.lean +++ b/Cslib/Foundations/Lint/Basic.lean @@ -4,8 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Henson -/ -import Batteries.Tactic.Lint.Basic -import Lean.Meta.GlobalInstances +module + +public import Batteries.Tactic.Lint.Basic +public meta import Lean.Meta.GlobalInstances namespace Cslib.Lint @@ -13,7 +15,7 @@ open Lean Meta Std Batteries.Tactic.Lint /-- A linter for checking that new declarations fall under some preexisting namespace. -/ @[env_linter] -def topNamespace : Batteries.Tactic.Lint.Linter where +meta def topNamespace : Batteries.Tactic.Lint.Linter where noErrorsFound := "No declarations are outside a namespace." errorsFound := "TOP LEVEL DECLARATIONS:" test declName := do diff --git a/Cslib/Foundations/Semantics/FLTS/Basic.lean b/Cslib/Foundations/Semantics/FLTS/Basic.lean index ba1843fb..c06cb59f 100644 --- a/Cslib/Foundations/Semantics/FLTS/Basic.lean +++ b/Cslib/Foundations/Semantics/FLTS/Basic.lean @@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Init +module + +public import Cslib.Init + +@[expose] public section /-! # Functional Labelled Transition System (FLTS) diff --git a/Cslib/Foundations/Semantics/FLTS/FLTSToLTS.lean b/Cslib/Foundations/Semantics/FLTS/FLTSToLTS.lean index ba3c25c2..0aeab4b8 100644 --- a/Cslib/Foundations/Semantics/FLTS/FLTSToLTS.lean +++ b/Cslib/Foundations/Semantics/FLTS/FLTSToLTS.lean @@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Foundations.Semantics.LTS.Basic -import Cslib.Foundations.Semantics.FLTS.Basic +module + +public import Cslib.Foundations.Semantics.LTS.Basic +public import Cslib.Foundations.Semantics.FLTS.Basic + +@[expose] public section variable {State Label : Type*} diff --git a/Cslib/Foundations/Semantics/FLTS/LTSToFLTS.lean b/Cslib/Foundations/Semantics/FLTS/LTSToFLTS.lean index afa6421b..036ea5ad 100644 --- a/Cslib/Foundations/Semantics/FLTS/LTSToFLTS.lean +++ b/Cslib/Foundations/Semantics/FLTS/LTSToFLTS.lean @@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Foundations.Semantics.LTS.Basic -import Cslib.Foundations.Semantics.FLTS.Basic +module + +public import Cslib.Foundations.Semantics.LTS.Basic +public import Cslib.Foundations.Semantics.FLTS.Basic + +@[expose] public section variable {State Label : Type*} diff --git a/Cslib/Foundations/Semantics/FLTS/Prod.lean b/Cslib/Foundations/Semantics/FLTS/Prod.lean index 5ce1680a..115b01be 100644 --- a/Cslib/Foundations/Semantics/FLTS/Prod.lean +++ b/Cslib/Foundations/Semantics/FLTS/Prod.lean @@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Ching-Tsun Chou, Fabrizio Montesi -/ -import Cslib.Foundations.Semantics.FLTS.Basic +module + +public import Cslib.Foundations.Semantics.FLTS.Basic + +@[expose] public section /-! # Product of functional labelled transition systems -/ diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean index e29c98c8..50e81fbc 100644 --- a/Cslib/Foundations/Semantics/LTS/Basic.lean +++ b/Cslib/Foundations/Semantics/LTS/Basic.lean @@ -4,10 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Init -import Mathlib.Data.Set.Finite.Basic -import Mathlib.Order.ConditionallyCompleteLattice.Basic -import Cslib.Foundations.Data.OmegaSequence.Init +module + +public import Cslib.Init +public import Mathlib.Data.Set.Finite.Basic +public import Mathlib.Order.ConditionallyCompleteLattice.Basic +public import Cslib.Foundations.Data.OmegaSequence.Init + +@[expose] public section /-! # Labelled Transition System (LTS) @@ -677,6 +681,8 @@ class LTS.DivergenceFree [HasTau Label] (lts : LTS State Label) where end Divergence +meta section + open Lean Elab Meta Command Term /-- A command to create an `LTS` from a labelled transition `α → β → α → Prop`, robust to use of @@ -762,4 +768,6 @@ initialize Lean.registerBuiltinAttribute { | _ => throwError "invalid syntax for 'lts' attribute" } +end + end Cslib diff --git a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean index 42f6f921..412a1559 100644 --- a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean @@ -4,9 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Foundations.Data.Relation -import Cslib.Foundations.Semantics.LTS.Simulation -import Cslib.Foundations.Semantics.LTS.TraceEq +module + +public import Cslib.Foundations.Data.Relation +public import Cslib.Foundations.Semantics.LTS.Simulation +public import Cslib.Foundations.Semantics.LTS.TraceEq + +@[expose] public section /-! # Bisimulation and Bisimilarity diff --git a/Cslib/Foundations/Semantics/LTS/Simulation.lean b/Cslib/Foundations/Semantics/LTS/Simulation.lean index c60e82f4..5cbdbe6d 100644 --- a/Cslib/Foundations/Semantics/LTS/Simulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Simulation.lean @@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Foundations.Semantics.LTS.Basic +module + +public import Cslib.Foundations.Semantics.LTS.Basic + +@[expose] public section /-! # Simulation and Similarity diff --git a/Cslib/Foundations/Semantics/LTS/TraceEq.lean b/Cslib/Foundations/Semantics/LTS/TraceEq.lean index 6826bc56..9c9f1061 100644 --- a/Cslib/Foundations/Semantics/LTS/TraceEq.lean +++ b/Cslib/Foundations/Semantics/LTS/TraceEq.lean @@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Foundations.Semantics.LTS.Basic +module + +public import Cslib.Foundations.Semantics.LTS.Basic + +@[expose] public section /-! # Trace Equivalence diff --git a/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean b/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean index 1eae39b2..5aad8a38 100644 --- a/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean +++ b/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean @@ -4,9 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi, Thomas Waring -/ -import Cslib.Init -import Mathlib.Logic.Relation -import Mathlib.Util.Notation3 +module + +public import Cslib.Init +public import Mathlib.Logic.Relation +public import Mathlib.Util.Notation3 + +@[expose] public section /-! # Reduction System diff --git a/Cslib/Foundations/Syntax/HasAlphaEquiv.lean b/Cslib/Foundations/Syntax/HasAlphaEquiv.lean index e32b1263..75218d4b 100644 --- a/Cslib/Foundations/Syntax/HasAlphaEquiv.lean +++ b/Cslib/Foundations/Syntax/HasAlphaEquiv.lean @@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Init +module + +public import Cslib.Init + +@[expose] public section namespace Cslib diff --git a/Cslib/Foundations/Syntax/HasSubstitution.lean b/Cslib/Foundations/Syntax/HasSubstitution.lean index 5ec1ce84..e37dbe5e 100644 --- a/Cslib/Foundations/Syntax/HasSubstitution.lean +++ b/Cslib/Foundations/Syntax/HasSubstitution.lean @@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Init +module + +public import Cslib.Init + +@[expose] public section namespace Cslib diff --git a/Cslib/Foundations/Syntax/HasWellFormed.lean b/Cslib/Foundations/Syntax/HasWellFormed.lean index 1e720fda..37a3d731 100644 --- a/Cslib/Foundations/Syntax/HasWellFormed.lean +++ b/Cslib/Foundations/Syntax/HasWellFormed.lean @@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Init +module + +public import Cslib.Init + +@[expose] public section namespace Cslib diff --git a/Cslib/Init.lean b/Cslib/Init.lean index aab6277a..d62761ff 100644 --- a/Cslib/Init.lean +++ b/Cslib/Init.lean @@ -4,9 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jesse Alama -/ -import Cslib.Foundations.Lint.Basic -import Mathlib.Init -import Mathlib.Tactic.Common +module + +public import Cslib.Foundations.Lint.Basic +public import Mathlib.Init +public import Mathlib.Tactic.Common /-! # CSLib Initialization diff --git a/Cslib/Languages/CCS/Basic.lean b/Cslib/Languages/CCS/Basic.lean index 2b119190..776a4d86 100644 --- a/Cslib/Languages/CCS/Basic.lean +++ b/Cslib/Languages/CCS/Basic.lean @@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Init +module + +public import Cslib.Init + +@[expose] public section /-! # Calculus of Communicating Systems (CCS) diff --git a/Cslib/Languages/CCS/BehaviouralTheory.lean b/Cslib/Languages/CCS/BehaviouralTheory.lean index c624a308..3cbdf1f7 100644 --- a/Cslib/Languages/CCS/BehaviouralTheory.lean +++ b/Cslib/Languages/CCS/BehaviouralTheory.lean @@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Foundations.Semantics.LTS.Bisimulation -import Cslib.Languages.CCS.Semantics +module + +public import Cslib.Foundations.Semantics.LTS.Bisimulation +public import Cslib.Languages.CCS.Semantics + +@[expose] public section /-! # Behavioural theory of CCS diff --git a/Cslib/Languages/CCS/Semantics.lean b/Cslib/Languages/CCS/Semantics.lean index caad83ad..09dfb341 100644 --- a/Cslib/Languages/CCS/Semantics.lean +++ b/Cslib/Languages/CCS/Semantics.lean @@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Foundations.Semantics.LTS.Basic -import Cslib.Languages.CCS.Basic +module + +public import Cslib.Foundations.Semantics.LTS.Basic +public import Cslib.Languages.CCS.Basic + +@[expose] public section /-! # Semantics of CCS diff --git a/Cslib/Languages/CombinatoryLogic/Basic.lean b/Cslib/Languages/CombinatoryLogic/Basic.lean index 07cea92a..09897c5e 100644 --- a/Cslib/Languages/CombinatoryLogic/Basic.lean +++ b/Cslib/Languages/CombinatoryLogic/Basic.lean @@ -3,7 +3,12 @@ Copyright (c) 2025 Thomas Waring. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Thomas Waring -/ -import Cslib.Languages.CombinatoryLogic.Defs + +module + +public import Cslib.Languages.CombinatoryLogic.Defs + +@[expose] public section /-! # Basic results for the SKI calculus diff --git a/Cslib/Languages/CombinatoryLogic/Confluence.lean b/Cslib/Languages/CombinatoryLogic/Confluence.lean index 3694fb6b..03a79030 100644 --- a/Cslib/Languages/CombinatoryLogic/Confluence.lean +++ b/Cslib/Languages/CombinatoryLogic/Confluence.lean @@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Thomas Waring -/ -import Cslib.Foundations.Data.Relation -import Cslib.Languages.CombinatoryLogic.Defs +module + +public import Cslib.Foundations.Data.Relation +public import Cslib.Languages.CombinatoryLogic.Defs + +@[expose] public section /-! # SKI reduction is confluent diff --git a/Cslib/Languages/CombinatoryLogic/Defs.lean b/Cslib/Languages/CombinatoryLogic/Defs.lean index 3cc6175b..b03f4fd5 100644 --- a/Cslib/Languages/CombinatoryLogic/Defs.lean +++ b/Cslib/Languages/CombinatoryLogic/Defs.lean @@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Thomas Waring -/ -import Cslib.Foundations.Semantics.ReductionSystem.Basic +module + +public meta import Cslib.Foundations.Semantics.ReductionSystem.Basic + +@[expose] public section /-! # SKI Combinatory Logic diff --git a/Cslib/Languages/CombinatoryLogic/Evaluation.lean b/Cslib/Languages/CombinatoryLogic/Evaluation.lean index eda48521..cbc48402 100644 --- a/Cslib/Languages/CombinatoryLogic/Evaluation.lean +++ b/Cslib/Languages/CombinatoryLogic/Evaluation.lean @@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Thomas Waring -/ -import Cslib.Languages.CombinatoryLogic.Confluence -import Cslib.Languages.CombinatoryLogic.Recursion +module + +public import Cslib.Languages.CombinatoryLogic.Confluence +public import Cslib.Languages.CombinatoryLogic.Recursion + +@[expose] public section /-! # Evaluation results diff --git a/Cslib/Languages/CombinatoryLogic/Recursion.lean b/Cslib/Languages/CombinatoryLogic/Recursion.lean index 173175dd..1b563ba0 100644 --- a/Cslib/Languages/CombinatoryLogic/Recursion.lean +++ b/Cslib/Languages/CombinatoryLogic/Recursion.lean @@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Thomas Waring -/ -import Cslib.Languages.CombinatoryLogic.Basic +module + +public import Cslib.Languages.CombinatoryLogic.Basic + +@[expose] public section /-! # General recursion in the SKI calculus diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean index 1d353fdc..3905e714 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean @@ -4,9 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Henson -/ -import Cslib.Foundations.Syntax.HasWellFormed -import Mathlib.Data.Finset.Dedup -import Mathlib.Data.List.Sigma +module + +public import Cslib.Foundations.Syntax.HasWellFormed +public import Mathlib.Data.Finset.Dedup +public import Mathlib.Data.List.Sigma + +@[expose] public section /-! # λ-calculus diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Basic.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Basic.lean index c0673b7b..37f686f9 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Basic.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Basic.lean @@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Henson -/ -import Cslib.Foundations.Data.HasFresh -import Cslib.Languages.LambdaCalculus.LocallyNameless.Context +module + +public import Cslib.Foundations.Data.HasFresh +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Context + +@[expose] public section /-! # λ-calculus diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean index 95339e1e..0e80f1bf 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean @@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Henson -/ -import Cslib.Foundations.Syntax.HasSubstitution -import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Basic +module + +public import Cslib.Foundations.Syntax.HasSubstitution +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Basic + +@[expose] public section set_option linter.unusedDecidableInType false diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Reduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Reduction.lean index 499b968b..04264bda 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Reduction.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Reduction.lean @@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Henson -/ -import Cslib.Foundations.Semantics.ReductionSystem.Basic -import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Opening +module + +public meta import Cslib.Foundations.Semantics.ReductionSystem.Basic +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Opening + +@[expose] public section set_option linter.unusedDecidableInType false @@ -106,7 +110,7 @@ inductive Red : Term Var → Term Var → Prop | case_inr : Value t₁ → t₂.body → t₃.body → Red (case (inr t₁) t₂ t₃) (t₃ ^ᵗᵗ t₁) @[grind _=_] -private lemma rs_eq {t t' : Term Var} : t ⭢βᵛ t' ↔ Red t t' := by +lemma rs_eq {t t' : Term Var} : t ⭢βᵛ t' ↔ Red t t' := by have : (@rs Var).Red = Red := by rfl simp_all diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean index cd883f2f..3f18a724 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean @@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Henson -/ -import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Typing +module + +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Typing + +@[expose] public section /-! # λ-calculus diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean index a884a928..0081c816 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean @@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Henson -/ -import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.WellFormed +module + +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.WellFormed + +@[expose] public section /-! # λ-calculus diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean index 00378d61..085027f2 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean @@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Henson -/ -import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Reduction -import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Subtype +module + +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Reduction +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Subtype + +@[expose] public section /-! # λ-calculus diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean index adfa1a1a..6d0157fd 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean @@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Henson -/ -import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Opening +module + +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Opening + +@[expose] public section /-! # λ-calculus diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Basic.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Basic.lean index 827cc3e7..563d0574 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Basic.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Basic.lean @@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Henson -/ -import Cslib.Languages.LambdaCalculus.LocallyNameless.Context -import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties +module + +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Context +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties + +@[expose] public section set_option linter.unusedDecidableInType false diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Safety.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Safety.lean index 73ffbf93..3d27c716 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Safety.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Safety.lean @@ -4,9 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Henson -/ -import Cslib.Foundations.Data.Relation -import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic -import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta +module + +public import Cslib.Foundations.Data.Relation +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta + +@[expose] public section /-! # λ-calculus diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Basic.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Basic.lean index 6c97b0a1..8e4b44eb 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Basic.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Basic.lean @@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Henson -/ -import Cslib.Foundations.Data.HasFresh -import Cslib.Foundations.Syntax.HasSubstitution +module + +public import Cslib.Foundations.Data.HasFresh +public import Cslib.Foundations.Syntax.HasSubstitution + +@[expose] public section /-! # λ-calculus diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean index ae137bdf..9630deec 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean @@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Henson -/ -import Cslib.Foundations.Semantics.ReductionSystem.Basic -import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties +module + +public meta import Cslib.Foundations.Semantics.ReductionSystem.Basic +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties + +@[expose] public section set_option linter.unusedDecidableInType false @@ -47,7 +51,7 @@ variable {M M' N N' : Term Var} --- TODO: I think this could be generated along with the ReductionSystem @[scoped grind _=_] -private lemma fullBetaRs_Red_eq : M ⭢βᶠ N ↔ FullBeta M N := by +lemma fullBetaRs_Red_eq : M ⭢βᶠ N ↔ FullBeta M N := by have : (@fullBetaRs Var).Red = FullBeta := by rfl simp_all diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean index eb017a87..0eaff53f 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean @@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Henson -/ -import Cslib.Foundations.Data.Relation -import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta +module + +public import Cslib.Foundations.Data.Relation +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta + +@[expose] public section set_option linter.unusedDecidableInType false diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean index 9fef37d5..250300bf 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean @@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Henson -/ -import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic +module + +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic + +@[expose] public section namespace Cslib diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean index 611718a1..c6adcca3 100644 --- a/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean +++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean @@ -4,9 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Foundations.Data.HasFresh -import Cslib.Foundations.Syntax.HasAlphaEquiv -import Cslib.Foundations.Syntax.HasSubstitution +module + +public import Cslib.Foundations.Data.HasFresh +public import Cslib.Foundations.Syntax.HasAlphaEquiv +public import Cslib.Foundations.Syntax.HasSubstitution + +@[expose] public section /-! # λ-calculus diff --git a/Cslib/Logics/LinearLogic/CLL/Basic.lean b/Cslib/Logics/LinearLogic/CLL/Basic.lean index c82540e3..9f720bdb 100644 --- a/Cslib/Logics/LinearLogic/CLL/Basic.lean +++ b/Cslib/Logics/LinearLogic/CLL/Basic.lean @@ -4,12 +4,16 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Init -import Mathlib.Order.Notation -import Mathlib.Order.Defs.Unbundled -import Mathlib.Data.Multiset.Defs -import Mathlib.Data.Multiset.Fold -import Mathlib.Data.Multiset.AddSub +module + +public import Cslib.Init +public import Mathlib.Order.Notation +public import Mathlib.Order.Defs.Unbundled +public import Mathlib.Data.Multiset.Defs +public import Mathlib.Data.Multiset.Fold +public import Mathlib.Data.Multiset.AddSub + +@[expose] public section /-! # Classical Linear Logic diff --git a/Cslib/Logics/LinearLogic/CLL/CutElimination.lean b/Cslib/Logics/LinearLogic/CLL/CutElimination.lean index 77aa7582..7969a7d6 100644 --- a/Cslib/Logics/LinearLogic/CLL/CutElimination.lean +++ b/Cslib/Logics/LinearLogic/CLL/CutElimination.lean @@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Logics.LinearLogic.CLL.Basic +module + +public import Cslib.Logics.LinearLogic.CLL.Basic + +@[expose] public section namespace Cslib diff --git a/Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean b/Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean index be987641..d1e08170 100644 --- a/Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean +++ b/Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean @@ -4,7 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Logics.LinearLogic.CLL.Basic +module + +public import Cslib.Logics.LinearLogic.CLL.Basic + +@[expose] public section /-! # η-expansion for Classical Linear Logic (CLL) -/ diff --git a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean index c508cb08..971c4353 100644 --- a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean +++ b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean @@ -3,12 +3,17 @@ Copyright (c) 2025 Tanner Duve. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Tanner Duve, Bhavik Mehta -/ -import Mathlib.Algebra.Group.Defs -import Mathlib.Algebra.Group.Pointwise.Set.Basic -import Mathlib.Algebra.Group.Idempotent -import Mathlib.Data.Set.Basic -import Mathlib.Order.Closure -import Cslib.Logics.LinearLogic.CLL.Basic + +module + +public import Mathlib.Algebra.Group.Defs +public import Mathlib.Algebra.Group.Pointwise.Set.Basic +public import Mathlib.Algebra.Group.Idempotent +public import Mathlib.Data.Set.Basic +public import Mathlib.Order.Closure +public import Cslib.Logics.LinearLogic.CLL.Basic + +@[expose] public section /-! # Phase semantics for Classical Linear Logic From b4191b1023005eb8b87442183901f447b0d553ed Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Sat, 3 Jan 2026 11:26:45 -0600 Subject: [PATCH 2/5] lake exe mk_all --check --module --- .github/workflows/lean_action_ci.yml | 4 ++++ CslibTests.lean | 22 ++++++++++++---------- 2 files changed, 16 insertions(+), 10 deletions(-) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index e51fdbef..f0de7d7d 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -18,6 +18,10 @@ jobs: with: build-args: "--wfail --iofail" mk_all-check: "true" + - name: "lake exe mk_all --check --module" + run: | + set -e + lake exe mk_all --check --module - name: "lake exe shake" run: | set -e diff --git a/CslibTests.lean b/CslibTests.lean index 20656f5f..e1aaeff0 100644 --- a/CslibTests.lean +++ b/CslibTests.lean @@ -1,10 +1,12 @@ -import CslibTests.Bisimulation -import CslibTests.CCS -import CslibTests.DFA -import CslibTests.FreeMonad -import CslibTests.GrindLint -import CslibTests.HasFresh -import CslibTests.ImportWithMathlib -import CslibTests.LTS -import CslibTests.LambdaCalculus -import CslibTests.ReductionSystem +module + +public import CslibTests.Bisimulation +public import CslibTests.CCS +public import CslibTests.DFA +public import CslibTests.FreeMonad +public import CslibTests.GrindLint +public import CslibTests.HasFresh +public import CslibTests.ImportWithMathlib +public import CslibTests.LTS +public import CslibTests.LambdaCalculus +public import CslibTests.ReductionSystem From b6930e0ba5a5f27830fa9a6190dc7daaf19f2145 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Sat, 3 Jan 2026 11:29:53 -0600 Subject: [PATCH 3/5] rm old param --- .github/workflows/lean_action_ci.yml | 1 - 1 file changed, 1 deletion(-) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index f0de7d7d..d530b4b8 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -17,7 +17,6 @@ jobs: - uses: leanprover/lean-action@v1 with: build-args: "--wfail --iofail" - mk_all-check: "true" - name: "lake exe mk_all --check --module" run: | set -e From b28282c18d22d0ad427ccb8e9dbc552775b6fb87 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Sat, 3 Jan 2026 11:43:15 -0600 Subject: [PATCH 4/5] rm shake from CI --- .github/workflows/lean_action_ci.yml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index d530b4b8..25e526df 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -21,10 +21,10 @@ jobs: run: | set -e lake exe mk_all --check --module - - name: "lake exe shake" - run: | - set -e - lake exe shake Cslib + #- name: "lake exe shake" + # run: | + # set -e + # lake exe shake Cslib - uses: leanprover-community/lint-style-action@main with: mode: check From 9845efcad114293eefc2fa8d28cd53b5148ca6d3 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Mon, 5 Jan 2026 10:50:24 -0500 Subject: [PATCH 5/5] rm expose in files without def/instance --- Cslib/Computability/Automata/DA/Buchi.lean | 2 +- Cslib/Foundations/Syntax/HasAlphaEquiv.lean | 2 +- Cslib/Foundations/Syntax/HasSubstitution.lean | 2 +- Cslib/Foundations/Syntax/HasWellFormed.lean | 2 +- Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean | 2 +- .../LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean | 2 +- .../LambdaCalculus/LocallyNameless/Untyped/Properties.lean | 2 +- 7 files changed, 7 insertions(+), 7 deletions(-) diff --git a/Cslib/Computability/Automata/DA/Buchi.lean b/Cslib/Computability/Automata/DA/Buchi.lean index ce4d4c66..f793154c 100644 --- a/Cslib/Computability/Automata/DA/Buchi.lean +++ b/Cslib/Computability/Automata/DA/Buchi.lean @@ -8,7 +8,7 @@ module public import Cslib.Computability.Automata.DA.Basic -@[expose] public section +public section /-! # Deterministic Buchi automata. -/ diff --git a/Cslib/Foundations/Syntax/HasAlphaEquiv.lean b/Cslib/Foundations/Syntax/HasAlphaEquiv.lean index 75218d4b..59dbd926 100644 --- a/Cslib/Foundations/Syntax/HasAlphaEquiv.lean +++ b/Cslib/Foundations/Syntax/HasAlphaEquiv.lean @@ -8,7 +8,7 @@ module public import Cslib.Init -@[expose] public section +public section namespace Cslib diff --git a/Cslib/Foundations/Syntax/HasSubstitution.lean b/Cslib/Foundations/Syntax/HasSubstitution.lean index e37dbe5e..77498359 100644 --- a/Cslib/Foundations/Syntax/HasSubstitution.lean +++ b/Cslib/Foundations/Syntax/HasSubstitution.lean @@ -8,7 +8,7 @@ module public import Cslib.Init -@[expose] public section +public section namespace Cslib diff --git a/Cslib/Foundations/Syntax/HasWellFormed.lean b/Cslib/Foundations/Syntax/HasWellFormed.lean index 37a3d731..f2ea7553 100644 --- a/Cslib/Foundations/Syntax/HasWellFormed.lean +++ b/Cslib/Foundations/Syntax/HasWellFormed.lean @@ -8,7 +8,7 @@ module public import Cslib.Init -@[expose] public section +public section namespace Cslib diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean index 3f18a724..e6baf9af 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean @@ -8,7 +8,7 @@ module public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Typing -@[expose] public section +public section /-! # λ-calculus diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean index 9630deec..ebda02b3 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean @@ -9,7 +9,7 @@ module public meta import Cslib.Foundations.Semantics.ReductionSystem.Basic public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties -@[expose] public section +public section set_option linter.unusedDecidableInType false diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean index 250300bf..ca3b3c44 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean @@ -8,7 +8,7 @@ module public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic -@[expose] public section +public section namespace Cslib