From ec3e35a32c107fccd6470a9818b26c702a55ff16 Mon Sep 17 00:00:00 2001
From: Bhargav Kulkarni <bhargav.kulkarni1@gmail.com>
Date: Thu, 22 Jan 2026 18:03:24 -0700
Subject: [PATCH 1/5] Adding proofs of correctness and time complexity of
 insertion sort

---
 .../Lean/InsertionSort/InsertionSort.lean     | 122 ++++++++++++++++++
 1 file changed, 122 insertions(+)
 create mode 100644 Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean

diff --git a/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean b/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean
new file mode 100644
index 00000000..1fbed9fc
--- /dev/null
+++ b/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean
@@ -0,0 +1,122 @@
+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
+
+set_option autoImplicit false
+
+namespace Cslib.Algorithms.Lean.TimeM
+
+variable {α : Type} [LinearOrder α]
+
+def insert : α → List α → TimeM (List α)
+| x, [] => return [x]
+| x, y :: ys => do
+  let c ← ✓ (x ≤ y : Bool)
+  if c then
+    return (x :: y :: ys)
+  else
+    let rest ← insert x ys
+    return (y :: rest)
+
+def insertionSort (xs : List α) : TimeM (List α) := do
+  match xs with
+  | [] => return []
+  | x :: xs' => do
+    let sortedTail ← insertionSort xs'
+    insert x sortedTail
+
+section Correctness
+
+open List
+
+@[grind →]
+theorem mem_either_insert (xs : List α) (a b : α) (hz : a ∈ ⟪insert b xs⟫) : a = b ∨ a ∈ xs := by
+  fun_induction insert with
+  | case1 _ => simp only [Pure.pure, pure, mem_cons, not_mem_nil, or_false] at hz; exact Or.inl hz
+  | case2 x y ys ih =>
+    simp_all only [Bind.bind, Pure.pure]
+    simp at hz
+    grind
+
+/-- A list is sorted if it satisfies the `Pairwise (· ≤ ·)` predicate. -/
+abbrev IsSorted (l : List α) : Prop := List.Pairwise (· ≤ ·) l
+
+theorem sorted_insert {x : α} {xs : List α} (hxs : IsSorted xs) :
+  IsSorted ⟪insert x xs⟫ := by
+  fun_induction insert x xs with
+  | case1 _ => simp
+  | case2 x y ys ih =>
+    simp only [Bind.bind, Pure.pure]
+    grind [pairwise_cons]
+
+theorem insertionSort_sorted (xs : List α) : IsSorted ⟪insertionSort xs⟫ := by
+  fun_induction insertionSort xs with
+  | case1 => simp
+  | case2 x xs ih =>
+    simp only [Bind.bind]
+    grind [sorted_insert]
+
+lemma insert_perm x (xs : List α) : ⟪insert x xs⟫ ~ x :: xs := by
+  fun_induction insert with
+  | case1 x => simp
+  | case2 x y ys ih =>
+    simp only [Bind.bind, Pure.pure]
+    grind
+
+theorem insertionSort_perm (xs : List α) : ⟪insertionSort xs⟫ ~ xs := by
+  fun_induction insertionSort xs with
+  | case1 => simp
+  | case2 x xs ih =>
+    simp only [Bind.bind, ret_bind]
+    refine (insert_perm x (insertionSort xs).ret).trans ?_
+    grind [List.Perm.cons]
+
+theorem insertionSort_correct (xs : List α) :
+    IsSorted ⟪insertionSort xs⟫ ∧ ⟪insertionSort xs⟫ ~ xs :=
+  ⟨insertionSort_sorted xs, insertionSort_perm xs⟩
+
+end Correctness
+
+section TimeComplexity
+
+theorem insert_time (x : α) (xs : List α) :
+    (insert x xs).time ≤ xs.length := by
+  fun_induction insert with
+  | case1 _ => simp
+  | case2 x y ys ih =>
+    simp [Bind.bind, Pure.pure]
+    grind
+
+theorem insert_length (x : α) (xs : List α) :
+    (insert x xs).ret.length = xs.length + 1 := by
+  fun_induction insert with
+  | case1 _ => simp
+  | case2 x y ys ih =>
+    simp [Bind.bind, Pure.pure]
+    grind
+
+theorem insertionSort_length (xs : List α) :
+    (insertionSort xs).ret.length = xs.length := by
+  fun_induction insertionSort xs with
+  | case1 => simp
+  | case2 x xs ih =>
+    simp [Bind.bind]
+    grind [insert_length]
+
+
+theorem insertionSort_time (xs : List α) :
+    (insertionSort xs).time ≤ xs.length * (xs.length + 1) / 2 := by
+  fun_induction insertionSort with
+  | case1 => simp
+  | case2 x xs ih =>
+    simp [Bind.bind]
+    grind [insert_time, insertionSort_length]
+
+end TimeComplexity
+
+end Cslib.Algorithms.Lean.TimeM

From 4880a7ce8162d10e1b6fb4895e43b0ecf39a163d Mon Sep 17 00:00:00 2001
From: Bhargav Kulkarni <bhargav.kulkarni1@gmail.com>
Date: Thu, 22 Jan 2026 18:10:46 -0700
Subject: [PATCH 2/5] Ammend the worst case complexity.

---
 Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean b/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean
index 1fbed9fc..d3072de3 100644
--- a/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean
+++ b/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean
@@ -110,7 +110,7 @@ theorem insertionSort_length (xs : List α) :
 
 
 theorem insertionSort_time (xs : List α) :
-    (insertionSort xs).time ≤ xs.length * (xs.length + 1) / 2 := by
+    (insertionSort xs).time ≤ xs.length * xs.length:= by
   fun_induction insertionSort with
   | case1 => simp
   | case2 x xs ih =>

From 9d94975302ab5c21f9049ed2f6e28821acba3b75 Mon Sep 17 00:00:00 2001
From: Bhargav Kulkarni <bhargav.kulkarni1@gmail.com>
Date: Sat, 24 Jan 2026 15:12:30 -0700
Subject: [PATCH 3/5] Making changes to fix CI error.

---
 Cslib.lean                                    | 159 +++++++++---------
 .../Lean/InsertionSort/InsertionSort.lean     |   6 +
 CslibTests.lean                               |  22 ++-
 3 files changed, 95 insertions(+), 92 deletions(-)

diff --git a/Cslib.lean b/Cslib.lean
index 8c6984eb..cfb1ecb8 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -1,80 +1,79 @@
-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.Loop
-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.Automata.NA.Total
-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
+import Cslib.Algorithms.Lean.InsertionSort.InsertionSort
+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.Loop
+import Cslib.Computability.Automata.NA.Prod
+import Cslib.Computability.Automata.NA.Sum
+import Cslib.Computability.Automata.NA.ToDA
+import Cslib.Computability.Automata.NA.Total
+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
diff --git a/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean b/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean
index d3072de3..e9317e14 100644
--- a/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean
+++ b/Cslib/Algorithms/Lean/InsertionSort/InsertionSort.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2026 Bhargav Kulkarni. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bhargav Kulkarni
+-/
+
 module
 
 public import Cslib.Algorithms.Lean.TimeM
diff --git a/CslibTests.lean b/CslibTests.lean
index e1aaeff0..20656f5f 100644
--- a/CslibTests.lean
+++ b/CslibTests.lean
@@ -1,12 +1,10 @@
-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
+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

From a1891f6f0397c56448dff7424d3f4158d220accc Mon Sep 17 00:00:00 2001
From: Bhargav Kulkarni <bhargav.kulkarni1@gmail.com>
Date: Sun, 25 Jan 2026 11:00:02 -0700
Subject: [PATCH 4/5] fixing conflicts

---
 Cslib.lean      | 2 ++
 CslibTests.lean | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/Cslib.lean b/Cslib.lean
index cfb1ecb8..df296455 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -1,3 +1,5 @@
+module
+
 import Cslib.Algorithms.Lean.InsertionSort.InsertionSort
 import Cslib.Algorithms.Lean.MergeSort.MergeSort
 import Cslib.Algorithms.Lean.TimeM
diff --git a/CslibTests.lean b/CslibTests.lean
index 20656f5f..ea03279f 100644
--- a/CslibTests.lean
+++ b/CslibTests.lean
@@ -1,3 +1,5 @@
+module
+
 import CslibTests.Bisimulation
 import CslibTests.CCS
 import CslibTests.DFA

From d796770153e0883a403234724a6f946484b553e3 Mon Sep 17 00:00:00 2001
From: Bhargav Kulkarni <bhargav.kulkarni1@gmail.com>
Date: Sun, 25 Jan 2026 11:01:51 -0700
Subject: [PATCH 5/5] fixing more conflicts

---
 Cslib.lean      | 158 ++++++++++++++++++++++++------------------------
 CslibTests.lean |  20 +++---
 2 files changed, 89 insertions(+), 89 deletions(-)

diff --git a/Cslib.lean b/Cslib.lean
index df296455..85aef6be 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -1,81 +1,81 @@
 module
 
-import Cslib.Algorithms.Lean.InsertionSort.InsertionSort
-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.Loop
-import Cslib.Computability.Automata.NA.Prod
-import Cslib.Computability.Automata.NA.Sum
-import Cslib.Computability.Automata.NA.ToDA
-import Cslib.Computability.Automata.NA.Total
-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
+public import Cslib.Algorithms.Lean.InsertionSort.InsertionSort
+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.Loop
+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.Automata.NA.Total
+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/CslibTests.lean b/CslibTests.lean
index ea03279f..e1aaeff0 100644
--- a/CslibTests.lean
+++ b/CslibTests.lean
@@ -1,12 +1,12 @@
 module
 
-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
+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