diff --git a/LSpec.lean b/LSpec.lean
index 50f1702..669c294 100644
--- a/LSpec.lean
+++ b/LSpec.lean
@@ -1,3 +1,4 @@
-import LSpec.LSpec
-import LSpec.Instances
-import LSpec.SlimCheck
+module
+public import LSpec.LSpec
+public import LSpec.Instances
+public import LSpec.SlimCheck
diff --git a/LSpec/Instances.lean b/LSpec/Instances.lean
index ca6c030..96cc0bf 100644
--- a/LSpec/Instances.lean
+++ b/LSpec/Instances.lean
@@ -1,4 +1,5 @@
-import LSpec.LSpec
+module
+public import LSpec.LSpec
 
 /-!
 # Testable Instances
@@ -16,6 +17,7 @@ LSpec to test equality, inequality, and bounded quantification directly.
 -/
 
 namespace LSpec
+public section
 
 /-- Testable instance for decidable equality. -/
 instance (priority := 50) (x y : α) [DecidableEq α] [Repr α] : Testable (x = y) :=
@@ -85,4 +87,5 @@ instance Nat.Testable_forall_lt
     | .isFalse h failedAt totalTests msg => .isFalse (λ h' => h λ n hn => h' _ (Nat.le_succ_of_le hn)) failedAt totalTests msg
     | .isFailure failedAt totalTests msg => .isFailure failedAt totalTests msg
 
+end
 end LSpec
diff --git a/LSpec/LSpec.lean b/LSpec/LSpec.lean
index f74267a..5f3a4d1 100644
--- a/LSpec/LSpec.lean
+++ b/LSpec/LSpec.lean
@@ -1,5 +1,5 @@
-import Lean
-import LSpec.SlimCheck.Checkable
+module
+public import LSpec.SlimCheck.Checkable
 
 /-!
 # The core `LSpec` framework
@@ -64,7 +64,7 @@ Use `check` and `checkIO` (without apostrophe) for simpler output.
 -/
 
 namespace LSpec
-
+public section
 /--
 The main typeclass of propositions that can be tested by `LSpec`.
 
@@ -585,4 +585,5 @@ def lspecEachIO (l : List α) (f : α → IO TestSeq) : IO UInt32 := do
     | (false, msg) => IO.eprintln msg; pure false
   if success then return 0 else return 1
 
+end
 end LSpec
diff --git a/LSpec/SlimCheck.lean b/LSpec/SlimCheck.lean
index 111b730..6761985 100644
--- a/LSpec/SlimCheck.lean
+++ b/LSpec/SlimCheck.lean
@@ -1,3 +1,4 @@
-import LSpec.SlimCheck.Gen
-import LSpec.SlimCheck.Checkable
-import LSpec.SlimCheck.Sampleable
+module
+public import LSpec.SlimCheck.Gen
+public import LSpec.SlimCheck.Checkable
+public import LSpec.SlimCheck.Sampleable
diff --git a/LSpec/SlimCheck/Checkable.lean b/LSpec/SlimCheck/Checkable.lean
index 9b3885b..e753820 100644
--- a/LSpec/SlimCheck/Checkable.lean
+++ b/LSpec/SlimCheck/Checkable.lean
@@ -4,8 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving, Simon Hudon
 -/
 
-import LSpec.SlimCheck.Sampleable
-import Lean
+module
+public import LSpec.SlimCheck.Sampleable
+public import Lean.Elab.Tactic.Basic
+meta import Lean.Elab.Tactic.Basic
 
 /-!
 # `Checkable` Class
@@ -61,7 +63,7 @@ random testing
 -/
 
 namespace SlimCheck
-
+public section
 /-- Result of trying to disprove `p`
 The constructors are:
   *  `success : (PSum Unit p) → TestResult p`
@@ -127,6 +129,7 @@ instance (priority := low) : PrintableProp p where
 class Checkable (p : Prop) where
   run (cfg : Configuration) (minimize : Bool) : Gen (TestResult p)
 
+@[expose]
 def NamedBinder (_n : String) (p : Prop) : Prop := p
 
 namespace TestResult
@@ -458,7 +461,7 @@ open Lean
 
 /-- Traverse the syntax of a proposition to find universal quantifiers
 quantifiers and add `NamedBinder` annotations next to them. -/
-partial def addDecorations (e : Expr) : Expr :=
+meta partial def addDecorations (e : Expr) : Expr :=
   e.replace fun expr => match expr with
     | Expr.forallE name type body data =>
       let n := name.toString
@@ -507,4 +510,5 @@ def Checkable.check (p : Prop) (cfg : Configuration := {})
 -- #eval Checkable.check (∀ (x : (Nat × Nat)), x.fst - x.snd - 10 = x.snd - x.fst - 10) Configuration.verbose
 -- #eval Checkable.check (∀ (x : Nat) (h : 10 < x), 5 < x) Configuration.verbose
 
+end
 end SlimCheck
diff --git a/LSpec/SlimCheck/Control/DefaultRange.lean b/LSpec/SlimCheck/Control/DefaultRange.lean
index 77fd585..6fa6bf4 100644
--- a/LSpec/SlimCheck/Control/DefaultRange.lean
+++ b/LSpec/SlimCheck/Control/DefaultRange.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Hanting Zhang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Hanting Zhang
 -/
+module
 
 /-!
 # Bounded and DefaultRange classes
@@ -29,6 +30,7 @@ Lean developers, please forgive us.
 -/
 
 namespace SlimCheck
+public section
 
 class Bounded (α : Type u) where
   lo : α
@@ -58,4 +60,5 @@ instance : DefaultRange Int where
   lo := - Int.ofNat (USize.size / 2)
   hi := Int.ofNat (USize.size / 2 - 1)
 
+end
 end SlimCheck
diff --git a/LSpec/SlimCheck/Control/Random.lean b/LSpec/SlimCheck/Control/Random.lean
index 126e351..cfa5fa7 100644
--- a/LSpec/SlimCheck/Control/Random.lean
+++ b/LSpec/SlimCheck/Control/Random.lean
@@ -3,7 +3,8 @@ Copyright (c) 2022 Henrik Böving. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-import LSpec.SlimCheck.Control.DefaultRange
+module
+public import LSpec.SlimCheck.Control.DefaultRange
 
 /-!
 # Rand Monad and Random Class
@@ -29,6 +30,7 @@ defining objects that can be created randomly.
 -/
 
 namespace SlimCheck
+public section
 
 /-- A monad to generate random objects using the generic generator type `g` -/
 abbrev RandT (g : Type) := StateM (ULift g)
@@ -133,4 +135,5 @@ def IO.runRand (cmd : Rand α) : BaseIO α := do
 def IO.runRandWith (seed : Nat) (cmd : Rand α) : BaseIO α := do
   pure $ (cmd.run (ULift.up $ mkStdGen seed)).1
 
+end
 end SlimCheck
diff --git a/LSpec/SlimCheck/Gen.lean b/LSpec/SlimCheck/Gen.lean
index 6eb089c..4b9aca4 100644
--- a/LSpec/SlimCheck/Gen.lean
+++ b/LSpec/SlimCheck/Gen.lean
@@ -3,7 +3,8 @@ Copyright (c) 2021 Henrik Böving. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving, Simon Hudon
 -/
-import LSpec.SlimCheck.Control.Random
+module
+public import LSpec.SlimCheck.Control.Random
 
 /-!
 # `Gen` Monad
@@ -19,6 +20,7 @@ random testing
 -/
 
 namespace SlimCheck
+public section
 
 open Random
 
@@ -118,4 +120,5 @@ end Gen
 def Gen.run (x : Gen α) (size : Nat) : BaseIO α :=
   IO.runRand $ ReaderT.run x ⟨size⟩
 
+end
 end SlimCheck
diff --git a/LSpec/SlimCheck/Sampleable.lean b/LSpec/SlimCheck/Sampleable.lean
index 999b24c..a4d5fe2 100644
--- a/LSpec/SlimCheck/Sampleable.lean
+++ b/LSpec/SlimCheck/Sampleable.lean
@@ -3,7 +3,8 @@ Copyright (c) 2022 Henrik Böving. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving, Simon Hudon
 -/
-import LSpec.SlimCheck.Gen
+module
+public import LSpec.SlimCheck.Gen
 
 /-!
 # `SampleableExt` Class
@@ -63,6 +64,7 @@ random testing
 -/
 
 namespace SlimCheck
+public section
 
 open Random
 
@@ -205,6 +207,7 @@ instance Prop.sampleableExt : SampleableExt Prop where
 end Samplers
 
 /-- An annotation for values that should never get shrinked. -/
+@[expose]
 def NoShrink (α : Type u) := α
 
 namespace NoShrink
@@ -223,4 +226,5 @@ instance sampleableExt [SampleableExt α] [Repr α] : SampleableExt (NoShrink α
 
 end NoShrink
 
+end
 end SlimCheck