Skip to content

chore: clean imports #725

New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Open
felixpernegger wants to merge 7 commits into
base: main
Choose a base branch
from
Open

chore: clean imports #725

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
4f9e2e5
.
felixpernegger Jul 17, 2026
eab0bc8
sort
felixpernegger Jul 17, 2026
7688248
init
felixpernegger Jul 17, 2026
bc93c5e
fix format
felixpernegger Jul 17, 2026
57a406b
include script
felixpernegger Jul 17, 2026
3f41c00
exclude again
felixpernegger Jul 17, 2026
9a35cbc
.
felixpernegger Jul 17, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
3 changes: 1 addition & 2 deletions Cslib/Computability/Languages/OmegaLanguage.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

/-!
Expand Down
2 changes: 1 addition & 1 deletion Cslib/Computability/Languages/OmegaRegularLanguage.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 1 addition & 3 deletions Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down
1 change: 0 additions & 1 deletion Cslib/Crypto/Protocols/PerfectSecrecy/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@ Authors: Samuel Schlesinger

module

public import Cslib.Crypto.Protocols.PerfectSecrecy.Defs
public import Cslib.Crypto.Protocols.PerfectSecrecy.Internal.PerfectSecrecy

/-!
Expand Down
1 change: 0 additions & 1 deletion Cslib/Crypto/Protocols/PerfectSecrecy/Defs.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 0 additions & 1 deletion Cslib/Crypto/Protocols/PerfectSecrecy/Internal/PerfectSecrecy.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 0 additions & 1 deletion Cslib/Crypto/Protocols/PerfectSecrecy/OneTimePad.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion Cslib/Crypto/Protocols/SecretSharing/Defs.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 0 additions & 1 deletion Cslib/Crypto/Protocols/SecretSharing/Scheme.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ Authors: Samuel Schlesinger
module

public import Cslib.Init
public import Mathlib.Data.Finset.Basic
public import Mathlib.Probability.ProbabilityMassFunction.Constructions

/-!
Expand Down
3 changes: 2 additions & 1 deletion Cslib/Crypto/Protocols/SecretSharing/Shamir.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

/-!
Expand Down
1 change: 0 additions & 1 deletion Cslib/Foundations/Combinatorics/InfiniteGraphRamsey.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
3 changes: 0 additions & 3 deletions Cslib/Foundations/Data/BiTape.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion Cslib/Foundations/Data/FinFun/Update.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion Cslib/Foundations/Data/HasFresh.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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. -/

Expand Down
1 change: 0 additions & 1 deletion Cslib/Foundations/Data/Nat/Segment.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

/-!
Expand Down
1 change: 0 additions & 1 deletion Cslib/Foundations/Data/OmegaSequence/Init.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

/-!
Expand Down
2 changes: 1 addition & 1 deletion Cslib/Foundations/Data/Set/Saturation.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 0 additions & 1 deletion Cslib/Foundations/Logic/LogicalEquivalence.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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. -/
Expand Down
3 changes: 1 addition & 2 deletions Cslib/Foundations/Relation/Attr.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
1 change: 0 additions & 1 deletion Cslib/Foundations/Relation/Defs.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
1 change: 0 additions & 1 deletion Cslib/Foundations/Relation/Restriction.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 0 additions & 1 deletion Cslib/Foundations/Semantics/LTS/Bisimulation.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
3 changes: 1 addition & 2 deletions Cslib/Foundations/Semantics/LTS/LTSCat/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
1 change: 0 additions & 1 deletion Cslib/Foundations/Semantics/LTS/TraceEq.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@ Authors: Fabrizio Montesi

module

public import Cslib.Foundations.Semantics.LTS.Basic
public import Cslib.Foundations.Semantics.LTS.Simulation

/-!
Expand Down
2 changes: 0 additions & 2 deletions Cslib/Languages/CCS/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down
2 changes: 1 addition & 1 deletion Cslib/Languages/CCS/Semantics.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions Cslib/Languages/CombinatoryLogic/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion Cslib/Languages/CombinatoryLogic/Confluence.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion Cslib/Languages/CombinatoryLogic/Defs.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Safety.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
6 changes: 1 addition & 5 deletions Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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. -/

Expand Down
1 change: 0 additions & 1 deletion Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 -/

Expand Down
1 change: 0 additions & 1 deletion Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 -/

Expand Down
2 changes: 0 additions & 2 deletions Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEtaConfluence.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 0 additions & 1 deletion Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 -/
Expand Down
2 changes: 1 addition & 1 deletion Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEtaConfluence.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
3 changes: 0 additions & 3 deletions Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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. -/

Expand Down
4 changes: 1 addition & 3 deletions Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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. -/

Expand Down
2 changes: 1 addition & 1 deletion Cslib/Logics/HML/LogicalEquivalence.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 0 additions & 2 deletions Cslib/Logics/LinearLogic/CLL/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading
Loading