diff --git a/Parser.lean b/Parser.lean
index 44c3621..4e301a7 100644
--- a/Parser.lean
+++ b/Parser.lean
@@ -2,11 +2,12 @@
 Copyright © 2022 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
+module
 
-import Parser.Basic
-import Parser.Char
-import Parser.Error
-import Parser.Parser
-import Parser.Prelude
-import Parser.RegEx
-import Parser.Stream
+public import Parser.Basic
+public import Parser.Char
+public import Parser.Error
+public import Parser.Parser
+public import Parser.Prelude
+public import Parser.RegEx
+public import Parser.Stream
diff --git a/Parser/Basic.lean b/Parser/Basic.lean
index 75d7d12..67787b6 100644
--- a/Parser/Basic.lean
+++ b/Parser/Basic.lean
@@ -2,11 +2,14 @@
 Copyright © 2022-2024 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
+module
 
 import Parser.Prelude
-import Parser.Error
-import Parser.Parser
-import Parser.Stream
+public import Parser.Error
+public import Parser.Parser
+public import Parser.Stream
+
+public section
 
 namespace Parser
 variable [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m]
diff --git a/Parser/Char.lean b/Parser/Char.lean
index 2fa485b..7074280 100644
--- a/Parser/Char.lean
+++ b/Parser/Char.lean
@@ -2,7 +2,8 @@
 Copyright © 2022-2023 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
+module
 
-import Parser.Char.Basic
-import Parser.Char.Numeric
-import Parser.Char.Unicode
+public import Parser.Char.Basic
+public import Parser.Char.Numeric
+public import Parser.Char.Unicode
diff --git a/Parser/Char/Basic.lean b/Parser/Char/Basic.lean
index 36fc71d..9ee07e4 100644
--- a/Parser/Char/Basic.lean
+++ b/Parser/Char/Basic.lean
@@ -2,10 +2,12 @@
 Copyright © 2022 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
+module
 
-import Parser.Basic
-import Parser.RegEx.Basic
+public import Parser.Basic
+public import Parser.RegEx.Basic
 
+public section
 namespace Parser.Char
 variable {ε σ m} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m]
 
diff --git a/Parser/Char/Numeric.lean b/Parser/Char/Numeric.lean
index 893735a..b8ccdf5 100644
--- a/Parser/Char/Numeric.lean
+++ b/Parser/Char/Numeric.lean
@@ -2,10 +2,12 @@
 Copyright © 2022-2023 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
+module
 
-import Parser.Basic
-import Parser.Char.Basic
+public import Parser.Basic
+public import Parser.Char.Basic
 
+public section
 namespace Parser.Char.ASCII
 variable {ε σ m} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m]
 
diff --git a/Parser/Char/Unicode.lean b/Parser/Char/Unicode.lean
index 37bd7ef..b55ce23 100644
--- a/Parser/Char/Unicode.lean
+++ b/Parser/Char/Unicode.lean
@@ -2,9 +2,11 @@
 Copyright © 2022 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
+module
 
-import Parser.Char.Basic
+public import Parser.Char.Basic
 
+public section
 namespace Parser.Char.Unicode
 variable {ε σ m} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m]
 
diff --git a/Parser/Error.lean b/Parser/Error.lean
index 3c64e0b..50b5e11 100644
--- a/Parser/Error.lean
+++ b/Parser/Error.lean
@@ -2,9 +2,11 @@
 Copyright © 2022-2025 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
+module
 
 import Parser.Prelude
-import Parser.Stream
+public import Parser.Stream
+public section
 
 /-! # Parser Error
 
@@ -84,7 +86,7 @@ inductive Simple (σ τ) [Parser.Stream σ τ]
   | addMessage : Simple σ τ → Stream.Position σ → String → Simple σ τ
 
 -- The derive handler for `Repr` fails, this is a workaround.
-private def Simple.reprPrec {σ τ} [Parser.Stream σ τ] [Repr τ] [Repr (Stream.Position σ)] :
+protected def Simple.reprPrec {σ τ} [Parser.Stream σ τ] [Repr τ] [Repr (Stream.Position σ)] :
   Simple σ τ → Nat → Std.Format
   | unexpected pos a, prec =>
     Repr.addAppParen
@@ -102,7 +104,7 @@ private def Simple.reprPrec {σ τ} [Parser.Stream σ τ] [Repr τ] [Repr (Strea
         (Std.Format.nest (if prec >= max_prec then 1 else 2)
           (Std.Format.text "Parser.Error.Simple.addMessage" ++
             Std.Format.line ++
-            reprPrec e max_prec ++
+            Simple.reprPrec e max_prec ++
             Std.Format.line ++
             reprArg pos ++
             Std.Format.line ++
@@ -112,7 +114,7 @@ private def Simple.reprPrec {σ τ} [Parser.Stream σ τ] [Repr τ] [Repr (Strea
 instance (σ τ) [Parser.Stream σ τ] [Repr τ] [Repr (Stream.Position σ)] : Repr (Simple σ τ) where
   reprPrec := Simple.reprPrec
 
-private def Simple.toString {σ τ} [Repr τ] [Parser.Stream σ τ] [Repr (Parser.Stream.Position σ)] :
+protected def Simple.toString {σ τ} [Repr τ] [Parser.Stream σ τ] [Repr (Parser.Stream.Position σ)] :
   Simple σ τ → String
   | unexpected pos (some tok) => s!"unexpected token {repr tok} at {repr pos}"
   | unexpected pos none => s!"unexpected token at {repr pos}"
diff --git a/Parser/Parser.lean b/Parser/Parser.lean
index 80b6284..42e6ce5 100644
--- a/Parser/Parser.lean
+++ b/Parser/Parser.lean
@@ -2,10 +2,13 @@
 Copyright © 2022-2024 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
+module
 
 import Parser.Prelude
-import Parser.Error
-import Parser.Stream
+public import Parser.Error
+public import Parser.Stream
+
+public section
 
 /-- Parser result type. -/
 protected inductive Parser.Result.{u} (ε σ α : Type u) : Type u
@@ -19,6 +22,7 @@ protected inductive Parser.Result.{u} (ε σ α : Type u) : Type u
 `ParserT ε σ τ` is a monad transformer to parse tokens of type `τ` from the stream type `σ` with
 error type `ε`.
 -/
+@[expose]
 def ParserT (ε σ τ : Type _) [Parser.Stream σ τ] [Parser.Error ε σ τ] (m : Type _ → Type _)
   (α : Type _) : Type _ := σ → m (Parser.Result ε σ α)
 
diff --git a/Parser/Prelude.lean b/Parser/Prelude.lean
index 4ba90a1..8881c05 100644
--- a/Parser/Prelude.lean
+++ b/Parser/Prelude.lean
@@ -3,8 +3,9 @@ Copyright © 2022 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
 
-import Batteries
-import UnicodeBasic
+module
+public import Batteries
+public import UnicodeBasic
 
-instance : Std.Stream String.Slice Char where
+public instance : Std.Stream String.Slice Char where
   next? s := s.front? >>= fun c => return (c, s.drop 1)
diff --git a/Parser/RegEx.lean b/Parser/RegEx.lean
index 4127337..260c498 100644
--- a/Parser/RegEx.lean
+++ b/Parser/RegEx.lean
@@ -2,6 +2,7 @@
 Copyright © 2022-2023 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
+module
 
-import Parser.RegEx.Basic
-import Parser.RegEx.Compile
+public import Parser.RegEx.Basic
+public import Parser.RegEx.Compile
diff --git a/Parser/RegEx/Basic.lean b/Parser/RegEx/Basic.lean
index b0674d1..02fcfc9 100644
--- a/Parser/RegEx/Basic.lean
+++ b/Parser/RegEx/Basic.lean
@@ -3,9 +3,11 @@
 Copyright © 2022-2023 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
+module
 
-import Parser.Basic
+public import Parser.Basic
 
+public section
 namespace Parser
 
 /-- Type of regular expressions -/
diff --git a/Parser/RegEx/Compile.lean b/Parser/RegEx/Compile.lean
index 92e5452..501c4f7 100644
--- a/Parser/RegEx/Compile.lean
+++ b/Parser/RegEx/Compile.lean
@@ -2,10 +2,13 @@
 Copyright © 2022-2023 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
+module
 
 import Parser.Char
 import Parser.Char.Numeric
-import Parser.RegEx.Basic
+public import Parser.RegEx.Basic
+
+public section
 
 /-! ## RegEx Syntax
 
diff --git a/Parser/Stream.lean b/Parser/Stream.lean
index e1ae572..1d40c19 100644
--- a/Parser/Stream.lean
+++ b/Parser/Stream.lean
@@ -2,8 +2,9 @@
 Copyright © 2022-2025 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
-
-import Parser.Prelude
+module
+public import Parser.Prelude
+public section
 
 /-! # Parser Stream
 
@@ -42,6 +43,7 @@ attribute [inherit_doc Parser.Stream] Parser.Stream.getPosition Parser.Stream.se
 namespace Parser.Stream
 
 /-- Stream segment type. -/
+@[expose]
 def Segment (σ) [Parser.Stream σ τ] := Stream.Position σ × Stream.Position σ
 
 /-- Start position of stream segment. -/
@@ -55,7 +57,7 @@ abbrev Segment.stop [Parser.Stream σ τ] (s : Segment σ) := s.2
 This wrapper uses the entire stream state as position information; this is not efficient. Always
 prefer tailored `Parser.Stream` instances to this default.
 -/
-@[nolint unusedArguments]
+@[expose]
 def mkDefault (σ τ) [Std.Stream σ τ] := σ
 
 @[reducible]