Migrate to `Felix` namespaceHEADhotg

82 files changed, 491 insertions, 490 deletions

diff --git a/source/Felix/Cache/Codec.hs b/source/Felix/Cache/Codec.hs
index b216576..34f2694 100644
--- a/source/Felix/Cache/Codec.hs
+++ b/source/Felix/Cache/Codec.hs
@@ -49,7 +49,7 @@ module Felix.Cache.Codec
     ) where
 
 import Base hiding (Empty)
-import Checking.Core
+import Felix.Checking.Core
 import Felix.Math.Codec
 
 import Control.DeepSeq (NFData)
diff --git a/source/Checking/Authority.hs b/source/Felix/Checking/Authority.hs
index fb6cea0..58c123f 100644
--- a/source/Checking/Authority.hs
+++ b/source/Felix/Checking/Authority.hs
@@ -3,7 +3,7 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
 -- | Compact public fact authority and exact contextual authorization.
-module Checking.Authority
+module Felix.Checking.Authority
     ( EscapeKind(..)
     , EscapeKinds
     , emptyEscapeKinds
@@ -59,8 +59,8 @@ module Checking.Authority
     ) where
 
 import Base
-import Checking.Foundation
-import Checking.Identity
+import Felix.Checking.Foundation
+import Felix.Checking.Identity
 import Felix.Cache.Codec
 
 import Control.DeepSeq (NFData)
diff --git a/source/Checking/Backend/Problem.hs b/source/Felix/Checking/Backend/Problem.hs
index 8d3a071..0390020 100644
--- a/source/Checking/Backend/Problem.hs
+++ b/source/Felix/Checking/Backend/Problem.hs
@@ -2,7 +2,7 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
 -- | Complete-problem FOF/TH0 classification and construction.
-module Checking.Backend.Problem
+module Felix.Checking.Backend.Problem
     ( SupportedProposition
     , supportedProposition
     , projectSupportedProposition
@@ -55,8 +55,8 @@ module Checking.Backend.Problem
     ) where
 
 import Base
-import Checking.Core
-import Checking.Foundation
+import Felix.Checking.Core
+import Felix.Checking.Foundation
 
 import Control.Monad (foldM, unless)
 import Data.Bifunctor (first)
diff --git a/source/Checking/Backend/Tptp.hs b/source/Felix/Checking/Backend/Tptp.hs
index e70277e..a5c0546 100644
--- a/source/Checking/Backend/Tptp.hs
+++ b/source/Felix/Checking/Backend/Tptp.hs
@@ -2,7 +2,7 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
 -- | Deterministic task-wide TPTP preparation for checked typed problems.
-module Checking.Backend.Tptp
+module Felix.Checking.Backend.Tptp
     ( TypedFormulaOccurrence(..)
     , TypedTptpNameOrigin(..)
     , PreparedTypedTptpProblem
@@ -16,8 +16,8 @@ module Checking.Backend.Tptp
     ) where
 
 import Base hiding (Empty)
-import Checking.Backend.Problem
-import Checking.Core
+import Felix.Checking.Backend.Problem
+import Felix.Checking.Core
 import Tptp.UnsortedFirstOrder qualified as Tptp
 
 import Control.Monad (foldM)
diff --git a/source/Checking/Core.hs b/source/Felix/Checking/Core.hs
index bf5bf3b..13ec218 100644
--- a/source/Checking/Core.hs
+++ b/source/Felix/Checking/Core.hs
@@ -8,7 +8,7 @@
 --
 -- Scoped syntax is an operational construction language.  Only a checked,
 -- frozen value is semantic input to later kernel and backend boundaries.
-module Checking.Core
+module Felix.Checking.Core
     ( CoreType(..)
     , CoreIntrinsicTag(..)
     , coreIntrinsicType
diff --git a/source/Checking/Datatype.hs b/source/Felix/Checking/Datatype.hs
index a47f93d..66e64db 100644
--- a/source/Checking/Datatype.hs
+++ b/source/Felix/Checking/Datatype.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 {-# LANGUAGE NamedFieldPuns #-}
 
-module Checking.Datatype
+module Felix.Checking.Datatype
     ( CheckedDatatype
     , DatatypeValidationError
     , datatypeValidationErrorLocation
@@ -16,9 +16,9 @@ module Checking.Datatype
     ) where
 
 import Base
-import Report.Location
-import Syntax.Internal
-import Syntax.Lexicon
+import Felix.Report.Location
+import Felix.Syntax.Internal
+import Felix.Syntax.Lexicon
 
 import Data.List qualified as List
 import Data.List.NonEmpty qualified as NonEmpty
diff --git a/source/Checking/Declaration.hs b/source/Felix/Checking/Declaration.hs
index c1ecd55..15050c7 100644
--- a/source/Checking/Declaration.hs
+++ b/source/Felix/Checking/Declaration.hs
@@ -5,7 +5,7 @@
 {-# LANGUAGE RankNTypes #-}
 
 -- | Builder-confined authorization and atomic typed declaration append.
-module Checking.Declaration
+module Felix.Checking.Declaration
     ( ModuleDriver
     , DriverFailure(..)
     , DriverResult(..)
@@ -171,21 +171,21 @@ module Checking.Declaration
     ) where
 
 import Base
-import Checking.Authority
-import Checking.Backend.Problem qualified as Backend
-import Checking.Backend.Tptp qualified as Tptp
-import Checking.Core
-import Checking.Foundation
-import Checking.Identity
-import Checking.Kernel.Derivation
-import Checking.Materialization qualified as Materialization
-import Checking.Semantic
-import Checking.SetConstruction
 import Felix.Cache.Codec (encodeCache)
+import Felix.Checking.Authority
+import Felix.Checking.Backend.Problem qualified as Backend
+import Felix.Checking.Backend.Tptp qualified as Tptp
+import Felix.Checking.Core
+import Felix.Checking.Foundation
+import Felix.Checking.Identity
+import Felix.Checking.Kernel.Derivation
+import Felix.Checking.Materialization qualified as Materialization
+import Felix.Checking.Semantic
+import Felix.Checking.SetConstruction
 import Felix.Module
 import Felix.Provers qualified as Provers
-import Report.Location
-import Syntax.Abstract (StructSymbol)
+import Felix.Report.Location
+import Felix.Syntax.Abstract (StructSymbol)
 
 import Control.Exception qualified as Exception
 import Control.DeepSeq (deepseq)
diff --git a/source/Checking/Exact.hs b/source/Felix/Checking/Exact.hs
index 47e3859..c829743 100644
--- a/source/Checking/Exact.hs
+++ b/source/Felix/Checking/Exact.hs
@@ -2,7 +2,7 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
 -- | Direct compiler for the first exact monomorphic declaration family.
-module Checking.Exact
+module Felix.Checking.Exact
     ( ExactLocalId
     , exactLocalId
     , exactLocalIdValue
@@ -60,18 +60,18 @@ module Checking.Exact
     ) where
 
 import Base hiding (Empty)
-import Checking.Core
-import Checking.Declaration qualified as Declaration
-import Checking.Exact.Vocabulary
-import Checking.Identity
-import Checking.SetConstruction
-import Checking.Semantic
 import Felix.Cache.Codec
+import Felix.Checking.Core
+import Felix.Checking.Declaration qualified as Declaration
+import Felix.Checking.Exact.Vocabulary
+import Felix.Checking.Identity
+import Felix.Checking.Semantic
+import Felix.Checking.SetConstruction
 import Felix.Module
-import Report.Location
-import Syntax.Abstract qualified as Raw
-import Syntax.Interface (CanonicalLexicalEntry(..))
-import Syntax.Lexicon qualified as Lexicon
+import Felix.Report.Location
+import Felix.Syntax.Abstract qualified as Raw
+import Felix.Syntax.Interface (CanonicalLexicalEntry(..))
+import Felix.Syntax.Lexicon qualified as Lexicon
 
 import Control.Monad.Except (ExceptT)
 import Control.Monad.Except (MonadError, throwError)
diff --git a/source/Checking/Exact/Datatype.hs b/source/Felix/Checking/Exact/Datatype.hs
index 61d99e5..be943cd 100644
--- a/source/Checking/Exact/Datatype.hs
+++ b/source/Felix/Checking/Exact/Datatype.hs
@@ -3,7 +3,7 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
 -- | Exact preparation of deterministic datatype declarations.
-module Checking.Exact.Datatype
+module Felix.Checking.Exact.Datatype
     ( PreparedExactDatatype
     , preparedExactDatatypeObjects
     , preparedExactDatatypeBindings
@@ -23,22 +23,22 @@ module Checking.Exact.Datatype
     ) where
 
 import Base hiding (Empty)
-import Checking.Authority
-import Checking.Core
-import Checking.Datatype qualified as Datatype
-import Checking.Declaration qualified as Declaration
-import Checking.Exact.Global qualified as ExactGlobal
-import Checking.Exact.Vocabulary
-import Checking.Identity
-import Checking.Semantic
-import Checking.Typed.Inductive qualified as Typed
+import Felix.Checking.Authority
+import Felix.Checking.Core
+import Felix.Checking.Datatype qualified as Datatype
+import Felix.Checking.Declaration qualified as Declaration
+import Felix.Checking.Exact.Global qualified as ExactGlobal
+import Felix.Checking.Exact.Vocabulary
+import Felix.Checking.Identity
+import Felix.Checking.Semantic
+import Felix.Checking.Typed.Inductive qualified as Typed
 import Felix.Cache.Codec
 import Felix.Module
 import Felix.Meaning qualified as Meaning
-import Report.Location
-import Syntax.Abstract qualified as Raw
-import Syntax.Interface
-import Syntax.Internal qualified as Internal
+import Felix.Report.Location
+import Felix.Syntax.Abstract qualified as Raw
+import Felix.Syntax.Interface
+import Felix.Syntax.Internal qualified as Internal
 
 import Control.Monad (unless, when)
 import Control.Monad.Except (ExceptT)
diff --git a/source/Checking/Exact/Global.hs b/source/Felix/Checking/Exact/Global.hs
index 772a7e2..d4040e6 100644
--- a/source/Checking/Exact/Global.hs
+++ b/source/Felix/Checking/Exact/Global.hs
@@ -2,19 +2,19 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
 -- | Exact resolution of source symbols to checked semantic globals.
-module Checking.Exact.Global
+module Felix.Checking.Exact.Global
     ( ExactGlobalResolutionError(..)
     , resolveExactSourceGlobals
     ) where
 
 import Base
-import Checking.Core
-import Checking.Declaration qualified as Declaration
-import Checking.Exact.Vocabulary
-import Checking.Identity
-import Checking.Semantic
-import Checking.Typed.Inductive qualified as Typed
-import Syntax.Internal qualified as Internal
+import Felix.Checking.Core
+import Felix.Checking.Declaration qualified as Declaration
+import Felix.Checking.Exact.Vocabulary
+import Felix.Checking.Identity
+import Felix.Checking.Semantic
+import Felix.Checking.Typed.Inductive qualified as Typed
+import Felix.Syntax.Internal qualified as Internal
 
 import Control.Monad (foldM)
 import Control.Monad.Except
diff --git a/source/Checking/Exact/Inductive.hs b/source/Felix/Checking/Exact/Inductive.hs
index 441c773..5817b34 100644
--- a/source/Checking/Exact/Inductive.hs
+++ b/source/Felix/Checking/Exact/Inductive.hs
@@ -2,7 +2,7 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
 -- | Exact preparation and atomic publication of direct set inductives.
-module Checking.Exact.Inductive
+module Felix.Checking.Exact.Inductive
     ( PreparedExactInductive
     , preparedExactInductiveCarrierId
     , preparedExactInductiveCarrierType
@@ -19,21 +19,21 @@ module Checking.Exact.Inductive
     ) where
 
 import Base hiding (Empty)
-import Checking.Authority
-import Checking.Core
-import Checking.Declaration qualified as Declaration
-import Checking.Exact.Global qualified as ExactGlobal
-import Checking.Exact.Vocabulary
-import Checking.Foundation
-import Checking.Identity
-import Checking.Semantic
-import Checking.Typed.Inductive qualified as Typed
+import Felix.Checking.Authority
+import Felix.Checking.Core
+import Felix.Checking.Declaration qualified as Declaration
+import Felix.Checking.Exact.Global qualified as ExactGlobal
+import Felix.Checking.Exact.Vocabulary
+import Felix.Checking.Foundation
+import Felix.Checking.Identity
+import Felix.Checking.Semantic
+import Felix.Checking.Typed.Inductive qualified as Typed
 import Felix.Cache.Codec
 import Felix.Meaning qualified as Meaning
-import Report.Location
-import Syntax.Abstract qualified as Raw
-import Syntax.Interface
-import Syntax.Internal qualified as Internal
+import Felix.Report.Location
+import Felix.Syntax.Abstract qualified as Raw
+import Felix.Syntax.Interface
+import Felix.Syntax.Internal qualified as Internal
 
 import Control.Monad (unless, when)
 import Control.Monad.Except (ExceptT)
diff --git a/source/Checking/Exact/Proof.hs b/source/Felix/Checking/Exact/Proof.hs
index 92ff500..e2149c4 100644
--- a/source/Checking/Exact/Proof.hs
+++ b/source/Felix/Checking/Exact/Proof.hs
@@ -8,7 +8,7 @@
 -- become available and executes discharges depth-first.  The declaration
 -- boundary validates typed tasks and authority; it does not reconstruct this
 -- derivation.
-module Checking.Exact.Proof
+module Felix.Checking.Exact.Proof
     ( PreparedExactProof
     , preparedExactProofSyntaxId
     , preparedExactProofFirstOmission
@@ -27,20 +27,20 @@ module Checking.Exact.Proof
     ) where
 
 import Base
-import Checking.Authority qualified as Authority
-import Checking.Backend.Problem qualified as Backend
-import Checking.Core
-import Checking.Declaration qualified as Declaration
-import Checking.Exact qualified as Exact
-import Checking.Foundation
-import Checking.Identity
-import Checking.Kernel.Derivation (foundationFactDerivation)
-import Checking.Kernel.Proof qualified as KernelProof
-import Checking.SetConstruction
-import Checking.Semantic
+import Felix.Checking.Authority qualified as Authority
+import Felix.Checking.Backend.Problem qualified as Backend
+import Felix.Checking.Core
+import Felix.Checking.Declaration qualified as Declaration
+import Felix.Checking.Exact qualified as Exact
+import Felix.Checking.Foundation
+import Felix.Checking.Identity
+import Felix.Checking.Kernel.Derivation (foundationFactDerivation)
+import Felix.Checking.Kernel.Proof qualified as KernelProof
+import Felix.Checking.SetConstruction
+import Felix.Checking.Semantic
 import Felix.Cache.Codec
-import Report.Location
-import Syntax.Abstract qualified as Raw
+import Felix.Report.Location
+import Felix.Syntax.Abstract qualified as Raw
 
 import Control.Monad.Except (ExceptT)
 import Control.Monad.Except qualified as Except
diff --git a/source/Checking/Exact/Vocabulary.hs b/source/Felix/Checking/Exact/Vocabulary.hs
index 45a2844..a712bf1 100644
--- a/source/Checking/Exact/Vocabulary.hs
+++ b/source/Felix/Checking/Exact/Vocabulary.hs
@@ -2,7 +2,7 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
 -- | Semantic classification shared by the exact source compilers.
-module Checking.Exact.Vocabulary
+module Felix.Checking.Exact.Vocabulary
     ( FixedSemanticMeaning(..)
     , fixedSemanticMeaning
     , lowerFixedEqualityPredicate
@@ -13,11 +13,11 @@ module Checking.Exact.Vocabulary
     ) where
 
 import Base hiding (Empty)
-import Checking.Core
-import Checking.Semantic
-import Syntax.Abstract qualified as Raw
-import Syntax.Internal qualified as Internal
-import Syntax.Lexicon qualified as Lexicon
+import Felix.Checking.Core
+import Felix.Checking.Semantic
+import Felix.Syntax.Abstract qualified as Raw
+import Felix.Syntax.Internal qualified as Internal
+import Felix.Syntax.Lexicon qualified as Lexicon
 
 import Data.List.NonEmpty qualified as NonEmpty
 import Data.Map.Strict qualified as Map
diff --git a/source/Checking/FinalPrelude.hs b/source/Felix/Checking/FinalPrelude.hs
index acb3c7b..9cc43f4 100644
--- a/source/Checking/FinalPrelude.hs
+++ b/source/Felix/Checking/FinalPrelude.hs
@@ -3,7 +3,7 @@
 {-# LANGUAGE RankNTypes #-}
 
 -- | Authority-confined construction of the inert final-prelude candidate.
-module Checking.FinalPrelude
+module Felix.Checking.FinalPrelude
     ( FinalPreludeCandidate
     , finalPreludeParsed
     , finalPreludeSyntax
@@ -23,25 +23,25 @@ module Checking.FinalPrelude
     ) where
 
 import Base hiding (Empty)
-import Checking.Authority qualified as Authority
-import Checking.Core
-import Checking.Declaration qualified as Declaration
-import Checking.Exact qualified as Exact
-import Checking.Exact.Proof qualified as ExactProof
-import Checking.Foundation
-import Checking.Identity
-import Checking.SetConstruction
-import Checking.Semantic
-import Checking.Semantic qualified as Semantic
+import Felix.Checking.Authority qualified as Authority
+import Felix.Checking.Core
+import Felix.Checking.Declaration qualified as Declaration
+import Felix.Checking.Exact qualified as Exact
+import Felix.Checking.Exact.Proof qualified as ExactProof
+import Felix.Checking.Foundation
+import Felix.Checking.Identity
+import Felix.Checking.SetConstruction
+import Felix.Checking.Semantic
+import Felix.Checking.Semantic qualified as Semantic
 import Felix.Module
 import Felix.Cache.Codec (CacheDigest)
 import Felix.Parse
 import Felix.Prelude qualified as Prelude
 import Felix.Source (ImportRef)
-import Report.Location
-import Syntax.Abstract qualified as Raw
-import Syntax.Interface
-import Syntax.Lexicon qualified as Lexicon
+import Felix.Report.Location
+import Felix.Syntax.Abstract qualified as Raw
+import Felix.Syntax.Interface
+import Felix.Syntax.Lexicon qualified as Lexicon
 
 import Control.Monad (unless)
 import Data.Bifunctor (first)
diff --git a/source/Checking/Foundation.hs b/source/Felix/Checking/Foundation.hs
index 317d1b5..5852901 100644
--- a/source/Checking/Foundation.hs
+++ b/source/Felix/Checking/Foundation.hs
@@ -6,7 +6,7 @@
 -- Constructing 'CheckedFoundation' requires exact manifest coverage, closed
 -- well-typed schemas, and structural backend classification.  This gate
 -- certifies manifest conformance only; it is not a consistency proof.
-module Checking.Foundation
+module Felix.Checking.Foundation
     ( FoundationAxiomTag(..)
     , KernelRuleTag(..)
     , KernelRuleSignature(..)
@@ -32,7 +32,7 @@ module Checking.Foundation
     ) where
 
 import Base hiding (Empty)
-import Checking.Core
+import Felix.Checking.Core
 
 import Control.Monad (unless)
 import Data.List qualified as List
diff --git a/source/Checking/Identity.hs b/source/Felix/Checking/Identity.hs
index fe846dc..67347a3 100644
--- a/source/Checking/Identity.hs
+++ b/source/Felix/Checking/Identity.hs
@@ -3,7 +3,7 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
 -- | Content-addressed identities for checked mathematical content.
-module Checking.Identity
+module Felix.Checking.Identity
     ( TheoryId
     , theoryId
     , theoryIdDigest
@@ -67,8 +67,8 @@ module Checking.Identity
     ) where
 
 import Base
-import Checking.Core
-import Checking.Foundation
+import Felix.Checking.Core
+import Felix.Checking.Foundation
 import Felix.Cache.Codec
 import Felix.Math.Codec
 import Felix.Module
diff --git a/source/Checking/Kernel/Derivation.hs b/source/Felix/Checking/Kernel/Derivation.hs
index 65bcc25..e83b376 100644
--- a/source/Checking/Kernel/Derivation.hs
+++ b/source/Felix/Checking/Kernel/Derivation.hs
@@ -2,7 +2,7 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
 -- | Private in-memory proof trees and independent kernel replay.
-module Checking.Kernel.Derivation
+module Felix.Checking.Kernel.Derivation
     ( ImportIx
     , importIx
     , importIxValue
@@ -53,10 +53,10 @@ module Checking.Kernel.Derivation
     ) where
 
 import Base
-import Checking.Core
-import Checking.Foundation
-import Checking.Kernel.Semantics qualified as Semantics
-import Checking.Kernel.SetLfp qualified as SetLfp
+import Felix.Checking.Core
+import Felix.Checking.Foundation
+import Felix.Checking.Kernel.Semantics qualified as Semantics
+import Felix.Checking.Kernel.SetLfp qualified as SetLfp
 
 import Control.Monad (unless)
 import Data.Bifunctor (first)
diff --git a/source/Checking/Kernel/Proof.hs b/source/Felix/Checking/Kernel/Proof.hs
index 5fc0d96..d4ccedc 100644
--- a/source/Checking/Kernel/Proof.hs
+++ b/source/Felix/Checking/Kernel/Proof.hs
@@ -3,7 +3,7 @@
 
 -- | Small proof-producing natural-deduction combinators. Every resulting tree
 -- is still replayed independently before it can authorize a fact.
-module Checking.Kernel.Proof
+module Felix.Checking.Kernel.Proof
     ( ProofContext
     , rootProofContext
     , proofContextTypes
@@ -47,11 +47,11 @@ module Checking.Kernel.Proof
     ) where
 
 import Base
-import Checking.Core
-import Checking.Foundation
-import Checking.Kernel.Derivation
-import Checking.Kernel.Semantics qualified as Semantics
-import Checking.Kernel.SetLfp qualified as SetLfp
+import Felix.Checking.Core
+import Felix.Checking.Foundation
+import Felix.Checking.Kernel.Derivation
+import Felix.Checking.Kernel.Semantics qualified as Semantics
+import Felix.Checking.Kernel.SetLfp qualified as SetLfp
 
 import Control.Monad (unless)
 import Data.Bifunctor (first)
diff --git a/source/Checking/Kernel/Semantics.hs b/source/Felix/Checking/Kernel/Semantics.hs
index 3306b09..f9cfcfa 100644
--- a/source/Checking/Kernel/Semantics.hs
+++ b/source/Felix/Checking/Kernel/Semantics.hs
@@ -2,7 +2,7 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
 -- | Checked logical inference over scoped canonical HOL terms.
-module Checking.Kernel.Semantics
+module Felix.Checking.Kernel.Semantics
     ( implicationElimination
     , implicationIntroduction
     , forallElimination
@@ -17,7 +17,7 @@ module Checking.Kernel.Semantics
     ) where
 
 import Base
-import Checking.Core
+import Felix.Checking.Core
 
 import Control.Monad (unless)
 import Data.Bifunctor (first)
diff --git a/source/Checking/Kernel/SetLfp.hs b/source/Felix/Checking/Kernel/SetLfp.hs
index e3fa175..19f6714 100644
--- a/source/Checking/Kernel/SetLfp.hs
+++ b/source/Felix/Checking/Kernel/SetLfp.hs
@@ -2,7 +2,7 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
 -- | The four checked rules for the bounded set-valued least fixed point.
-module Checking.Kernel.SetLfp
+module Felix.Checking.Kernel.SetLfp
     ( setLfpBound
     , setLfpLeast
     , setLfpFixed
@@ -16,8 +16,8 @@ module Checking.Kernel.SetLfp
     ) where
 
 import Base
-import Checking.Core
-import Checking.Foundation
+import Felix.Checking.Core
+import Felix.Checking.Foundation
 
 import Data.Bifunctor (first)
 import Numeric.Natural (Natural)
diff --git a/source/Checking/Materialization.hs b/source/Felix/Checking/Materialization.hs
index 6dcf1f0..51944a5 100644
--- a/source/Checking/Materialization.hs
+++ b/source/Felix/Checking/Materialization.hs
@@ -5,7 +5,7 @@
 --
 -- Successful checks are inert. Fresh completion and validated loading or
 -- sealing own the runtime authority that may publish a fact.
-module Checking.Materialization
+module Felix.Checking.Materialization
     ( CandidateValidation
     , candidateProofValidation
     , candidateDeclarationValidation
@@ -17,9 +17,9 @@ module Checking.Materialization
     ) where
 
 import Base
-import Checking.Authority
-import Checking.Identity
-import Checking.Semantic
+import Felix.Checking.Authority
+import Felix.Checking.Identity
+import Felix.Checking.Semantic
 
 import Control.Monad (unless)
 import Numeric.Natural (Natural)
diff --git a/source/Checking/Module.hs b/source/Felix/Checking/Module.hs
index d0e1d52..88c8fef 100644
--- a/source/Checking/Module.hs
+++ b/source/Felix/Checking/Module.hs
@@ -3,7 +3,7 @@
 {-# LANGUAGE RankNTypes #-}
 
 -- | Explicit inputs and sealed outputs for the typed module driver.
-module Checking.Module
+module Felix.Checking.Module
     ( LiveModuleBinding(..)
     , IdentifiedModuleInput
     , identifiedPhysicalModule
@@ -55,23 +55,23 @@ module Checking.Module
     ) where
 
 import Base
-import Checking.Declaration qualified as Declaration
-import Checking.Exact qualified as Exact
-import Checking.Exact.Datatype qualified as ExactDatatype
-import Checking.Exact.Inductive qualified as ExactInductive
-import Checking.Exact.Proof qualified as ExactProof
-import Checking.FinalPrelude qualified as FinalPrelude
-import Checking.Foundation
-import Checking.Identity
-import Checking.Semantic
+import Felix.Checking.Declaration qualified as Declaration
+import Felix.Checking.Exact qualified as Exact
+import Felix.Checking.Exact.Datatype qualified as ExactDatatype
+import Felix.Checking.Exact.Inductive qualified as ExactInductive
+import Felix.Checking.Exact.Proof qualified as ExactProof
+import Felix.Checking.FinalPrelude qualified as FinalPrelude
+import Felix.Checking.Foundation
+import Felix.Checking.Identity
+import Felix.Checking.Semantic
 import Felix.Module
 import Felix.Parse
 import Felix.Prelude qualified as Prelude
 import Felix.Source
 import Felix.Store qualified as Store
-import Report.Location
-import Syntax.Interface
-import Syntax.Abstract qualified as Raw
+import Felix.Report.Location
+import Felix.Syntax.Interface
+import Felix.Syntax.Abstract qualified as Raw
 
 import Control.Monad (unless)
 import Data.Bifunctor (first)
diff --git a/source/Checking/Semantic.hs b/source/Felix/Checking/Semantic.hs
index 7a05f39..c9442f3 100644
--- a/source/Checking/Semantic.hs
+++ b/source/Felix/Checking/Semantic.hs
@@ -3,7 +3,7 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
 -- | Canonical semantic declaration, prefix, interface, and validation keys.
-module Checking.Semantic
+module Felix.Checking.Semantic
     ( DeclarationSlot
     , declarationSlot
     , declarationSlotModule
@@ -150,16 +150,16 @@ module Checking.Semantic
     ) where
 
 import Base
-import Checking.Authority
-import Checking.Core
-import Checking.Identity
+import Felix.Checking.Authority
+import Felix.Checking.Core
+import Felix.Checking.Identity
 import Felix.Cache.Codec
 import Felix.Math.Codec
 import Felix.Module
 import Felix.Parsed.Identity
 import Felix.Source
-import Syntax.Interface
-import Syntax.Abstract
+import Felix.Syntax.Interface
+import Felix.Syntax.Abstract
 
 import Control.DeepSeq (NFData)
 import Control.Monad (unless, when)
diff --git a/source/Checking/SetConstruction.hs b/source/Felix/Checking/SetConstruction.hs
index 4c4b4bc..a5e1d80 100644
--- a/source/Checking/SetConstruction.hs
+++ b/source/Felix/Checking/SetConstruction.hs
@@ -8,7 +8,7 @@
 -- telescope and derive one canonical term.  Local views, transparent content,
 -- direct extensional facts, and cache-scoped descriptors all consume that
 -- same checked value.
-module Checking.SetConstruction
+module Felix.Checking.SetConstruction
     ( NamedSetConstruction
     , checkedSeparationConstruction
     , checkedFunctionalReplacementConstruction
@@ -36,9 +36,9 @@ module Checking.SetConstruction
     ) where
 
 import Base hiding (Empty)
-import Checking.Core
-import Checking.Foundation
-import Checking.Identity
+import Felix.Checking.Core
+import Felix.Checking.Foundation
+import Felix.Checking.Identity
 import Felix.Cache.Codec
     ( CacheDigest
     , encodeCache
diff --git a/source/Checking/Typed/Inductive.hs b/source/Felix/Checking/Typed/Inductive.hs
index eb6c0f7..4094083 100644
--- a/source/Checking/Typed/Inductive.hs
+++ b/source/Felix/Checking/Typed/Inductive.hs
@@ -4,7 +4,7 @@
 
 -- | Direct checked lowering of the current one-carrier set-valued inductive
 -- declaration.
-module Checking.Typed.Inductive
+module Felix.Checking.Typed.Inductive
     ( DirectInductive(..)
     , DirectInductiveClause(..)
     , DirectInductiveCondition(..)
@@ -37,13 +37,13 @@ module Checking.Typed.Inductive
     ) where
 
 import Base hiding (Empty)
-import Checking.Core
-import Checking.Exact.Vocabulary
-import Checking.Foundation
-import Checking.Kernel.Derivation
-import Checking.Kernel.Proof
-import Report.Location (Location)
-import Syntax.Internal
+import Felix.Checking.Core
+import Felix.Checking.Exact.Vocabulary
+import Felix.Checking.Foundation
+import Felix.Checking.Kernel.Derivation
+import Felix.Checking.Kernel.Proof
+import Felix.Report.Location (Location)
+import Felix.Syntax.Internal
 
 import Control.Monad ((<=<), foldM)
 import Data.Bifunctor (first)
diff --git a/source/Felix/CommandLine.hs b/source/Felix/CommandLine.hs
index 701020f..448d698 100644
--- a/source/Felix/CommandLine.hs
+++ b/source/Felix/CommandLine.hs
@@ -26,10 +26,10 @@ import Felix.Store qualified as Store
 import Felix.Verification qualified as Verification
 import Felix.Version qualified as Version
 import Felix.Workspace qualified as Workspace
-import Render.Html.Export qualified as HtmlExport
-import Render.Html.Layout qualified as HtmlLayout
-import Render.Html.Output qualified as HtmlOutput
-import Report.Location
+import Felix.Render.Html.Export qualified as HtmlExport
+import Felix.Render.Html.Layout qualified as HtmlLayout
+import Felix.Render.Html.Output qualified as HtmlOutput
+import Felix.Report.Location
 
 import Control.Monad (unless, when)
 import Data.Maybe (catMaybes)
diff --git a/source/Felix/Math/Codec.hs b/source/Felix/Math/Codec.hs
index 4a5c7b1..a551f53 100644
--- a/source/Felix/Math/Codec.hs
+++ b/source/Felix/Math/Codec.hs
@@ -24,7 +24,7 @@ module Felix.Math.Codec
     ) where
 
 import Base hiding (Empty)
-import Checking.Core
+import Felix.Checking.Core
 
 import Control.DeepSeq (NFData)
 import Crypto.Hash qualified as Crypto
diff --git a/source/Felix/Meaning.hs b/source/Felix/Meaning.hs
index 60c4cfc..268a1a6 100644
--- a/source/Felix/Meaning.hs
+++ b/source/Felix/Meaning.hs
@@ -9,12 +9,12 @@ module Felix.Meaning where
 
 
 import Base
-import Syntax.Abstract (Sign(..))
-import Syntax.Abstract qualified as Raw
-import Syntax.Internal (VarSymbol(..), pattern FreshVar)
-import Syntax.Internal qualified as Sem
-import Syntax.LexicalPhrase (unsafeReadPhrase)
-import Report.Location
+import Felix.Syntax.Abstract (Sign(..))
+import Felix.Syntax.Abstract qualified as Raw
+import Felix.Syntax.Internal (VarSymbol(..), pattern FreshVar)
+import Felix.Syntax.Internal qualified as Sem
+import Felix.Syntax.LexicalPhrase (unsafeReadPhrase)
+import Felix.Report.Location
 
 import Bound
 import Control.Monad.Except
diff --git a/source/Felix/OutputPlan.hs b/source/Felix/OutputPlan.hs
index 58314db..78d7e7a 100644
--- a/source/Felix/OutputPlan.hs
+++ b/source/Felix/OutputPlan.hs
@@ -18,7 +18,7 @@ module Felix.OutputPlan
 import Base
 import Felix.Source
 import Felix.Store
-import Render.Html.Output qualified as Html
+import Felix.Render.Html.Output qualified as Html
 
 import Control.Exception (displayException)
 import Data.List qualified as List
diff --git a/source/Felix/Parse.hs b/source/Felix/Parse.hs
index e03feb9..0a46d82 100644
--- a/source/Felix/Parse.hs
+++ b/source/Felix/Parse.hs
@@ -90,9 +90,9 @@ import Felix.Source
 import Felix.Source.Content qualified as Content
 import Felix.Source.Graph
 import Felix.Store qualified as Store
-import Report.Location
-import Syntax.Abstract qualified as Raw
-import Syntax.Adapt
+import Felix.Report.Location
+import Felix.Syntax.Abstract qualified as Raw
+import Felix.Syntax.Adapt
     ( LexicalScanError(..)
     , ScannedLexicalItem
     , SyntaxMaterializationError(..)
@@ -101,11 +101,11 @@ import Syntax.Adapt
     , scanChunk
     , scannedItemMarker
     )
-import Syntax.Concrete (grammar)
-import Syntax.Interface
-import Syntax.Lexicon (Lexicon)
-import Syntax.Pragma
-import Syntax.Token
+import Felix.Syntax.Concrete (grammar)
+import Felix.Syntax.Interface
+import Felix.Syntax.Lexicon (Lexicon)
+import Felix.Syntax.Pragma
+import Felix.Syntax.Token
 
 import Control.DeepSeq (NFData, force)
 import Control.Exception (Exception, evaluate)
diff --git a/source/Felix/Parsed/Identity.hs b/source/Felix/Parsed/Identity.hs
index e11b2c7..b76c26e 100644
--- a/source/Felix/Parsed/Identity.hs
+++ b/source/Felix/Parsed/Identity.hs
@@ -20,7 +20,7 @@ module Felix.Parsed.Identity
 import Base
 import Felix.Cache.Codec
 import Felix.Source.Content
-import Syntax.Interface
+import Felix.Syntax.Interface
 
 import Control.DeepSeq (NFData)
 import Data.ByteString (ByteString)
diff --git a/source/Felix/Parsed/Payload.hs b/source/Felix/Parsed/Payload.hs
index 2506973..5e63c70 100644
--- a/source/Felix/Parsed/Payload.hs
+++ b/source/Felix/Parsed/Payload.hs
@@ -30,11 +30,11 @@ import Base
 import Felix.Cache.Codec
 import Felix.Parsed.Identity qualified as Identity
 import Felix.Source
-import Report.Location
-import Syntax.Abstract qualified as Raw
-import Syntax.Interface
-import Syntax.LexicalPhrase qualified as Phrase
-import Syntax.Token qualified as Token
+import Felix.Report.Location
+import Felix.Syntax.Abstract qualified as Raw
+import Felix.Syntax.Interface
+import Felix.Syntax.LexicalPhrase qualified as Phrase
+import Felix.Syntax.Token qualified as Token
 
 import Control.DeepSeq (NFData)
 import Control.Monad (unless)
diff --git a/source/Felix/Prelude.hs b/source/Felix/Prelude.hs
index 28ad961..ccd5623 100644
--- a/source/Felix/Prelude.hs
+++ b/source/Felix/Prelude.hs
@@ -30,10 +30,10 @@ import Felix.Parse
 import Felix.Parsed.Identity qualified as Parsed
 import Felix.Source
 import Felix.Source.Graph
-import Report.Location
-import Syntax.Adapt (SyntaxMaterializationError)
-import Syntax.Interface
-import Syntax.Pragma
+import Felix.Report.Location
+import Felix.Syntax.Adapt (SyntaxMaterializationError)
+import Felix.Syntax.Interface
+import Felix.Syntax.Pragma
 
 import Control.Exception (IOException, displayException, try)
 import Data.ByteString (ByteString)
diff --git a/source/Felix/Provers.hs b/source/Felix/Provers.hs
index eb6f62c..16ef655 100644
--- a/source/Felix/Provers.hs
+++ b/source/Felix/Provers.hs
@@ -79,9 +79,9 @@ module Felix.Provers
     ) where
 
 import Base
-import Checking.Authority qualified as Authority
-import Checking.Backend.Problem
-import Checking.Backend.Tptp
+import Felix.Checking.Authority qualified as Authority
+import Felix.Checking.Backend.Problem
+import Felix.Checking.Backend.Tptp
 
 import Control.Concurrent.STM
     ( STM
@@ -130,7 +130,7 @@ import Data.Text qualified as Text
 import Data.Text.Encoding qualified as TextEncoding
 import Data.Text.Encoding.Error qualified as TextEncodingError
 import Numeric.Natural (Natural)
-import Report.Location (Location)
+import Felix.Report.Location (Location)
 import System.Exit (ExitCode(..))
 import System.Posix.Signals (sigKILL, signalProcessGroup)
 import System.Posix.Types (ProcessGroupID)
diff --git a/source/Render/Html.hs b/source/Felix/Render/Html.hs
index c37a278..7081e52 100644
--- a/source/Render/Html.hs
+++ b/source/Felix/Render/Html.hs
@@ -3,7 +3,7 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE RecordWildCards #-}
 
-module Render.Html
+module Felix.Render.Html
     ( HtmlRenderIndex
     , HtmlPagePresentation
     , buildRenderIndex
@@ -12,14 +12,14 @@ module Render.Html
     , supportScriptAssetContents
     ) where
 
-import Syntax.Abstract
+import Felix.Syntax.Abstract
 
 import Base
 import Felix.Source (ResolvedSource)
 import Lucid hiding (Term, for_)
 import Lucid.Base (makeAttributes)
 import Lucid.Math
-import Render.Html.Context
+import Felix.Render.Html.Context
     ( HtmlRenderContext
     , HtmlRenderContextError
     , htmlCurrentPageLabel
@@ -29,7 +29,9 @@ import Render.Html.Context
     , htmlSourcePageHref
     , htmlSupportScriptHref
     )
-import Render.Html.Layout (renderUrlFragment)
+import Felix.Render.Html.Layout (renderUrlFragment)
+import Felix.Report.Location (Location, pattern Nowhere)
+import Felix.Syntax.Token (VariableDisplay(..), VariableSuffix(..), displayVariable, tokToText)
 
 import Control.Monad (unless, when)
 import Data.Char (digitToInt, isAlphaNum, isDigit, isSpace, toUpper)
@@ -39,8 +41,7 @@ import Data.Map.Strict qualified as Map
 import Data.Set qualified as Set
 import Data.Text qualified as Text
 import Data.Text.Lazy qualified as LazyText
-import Report.Location (Location, pattern Nowhere)
-import Syntax.Token (VariableDisplay(..), VariableSuffix(..), displayVariable, tokToText)
+
 
 
 data HintCategory
diff --git a/source/Render/Html/Context.hs b/source/Felix/Render/Html/Context.hs
index 151edd5..469d986 100644
--- a/source/Render/Html/Context.hs
+++ b/source/Felix/Render/Html/Context.hs
@@ -3,7 +3,7 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
 -- | Browser-facing routing authority for one rendered HTML page.
-module Render.Html.Context
+module Felix.Render.Html.Context
     ( HtmlRenderEnvironment
     , htmlRenderEnvironment
     , HtmlRenderContext
@@ -23,7 +23,7 @@ module Render.Html.Context
 
 import Base
 import Felix.Source
-import Render.Html.Layout
+import Felix.Render.Html.Layout
 
 import Control.Exception (Exception)
 import Data.Map.Strict qualified as Map
diff --git a/source/Render/Html/Export.hs b/source/Felix/Render/Html/Export.hs
index 2c747d8..a3f0e39 100644
--- a/source/Render/Html/Export.hs
+++ b/source/Felix/Render/Html/Export.hs
@@ -3,7 +3,7 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
 -- | Prepare a complete HTML export from retained parsed presentation.
-module Render.Html.Export
+module Felix.Render.Html.Export
     ( HtmlPresentation
     , htmlPresentationFromParsedWorkspace
     , HtmlExportError(..)
@@ -16,11 +16,11 @@ module Render.Html.Export
 import Base
 import Felix.Parse
 import Felix.Source
-import Render.Html qualified as Html
-import Render.Html.Context
-import Render.Html.Layout
-import Render.Html.Output
-import Syntax.Abstract (Block)
+import Felix.Render.Html qualified as Html
+import Felix.Render.Html.Context
+import Felix.Render.Html.Layout
+import Felix.Render.Html.Output
+import Felix.Syntax.Abstract (Block)
 
 import Control.Exception (Exception, IOException, displayException)
 import Control.Exception qualified as Exception
diff --git a/source/Render/Html/Layout.hs b/source/Felix/Render/Html/Layout.hs
index c26b6b5..7e5bfcf 100644
--- a/source/Render/Html/Layout.hs
+++ b/source/Felix/Render/Html/Layout.hs
@@ -2,7 +2,7 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
 -- | Pure browser and destination routing for a resolved source graph.
-module Render.Html.Layout
+module Felix.Render.Html.Layout
     ( UrlSegment
     , UrlSegmentError(..)
     , urlSegment
diff --git a/source/Render/Html/Output.hs b/source/Felix/Render/Html/Output.hs
index 685c83a..8e36f97 100644
--- a/source/Render/Html/Output.hs
+++ b/source/Felix/Render/Html/Output.hs
@@ -8,7 +8,7 @@
 -- accepted only when they resolve inside the canonical root. Final-target
 -- symlinks are rejected without following them; regular generated files may be
 -- replaced. This policy prevents stable-tree escapes, not TOCTOU attacks.
-module Render.Html.Output
+module Felix.Render.Html.Output
     ( PreparedHtmlArtifact
     , preparedHtmlArtifact
     , preparedHtmlArtifactDestination
diff --git a/source/Report/Location.hs b/source/Felix/Report/Location.hs
index 4495360..36b8997 100644
--- a/source/Report/Location.hs
+++ b/source/Felix/Report/Location.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DerivingStrategies #-}
 
-module Report.Location where
+module Felix.Report.Location where
 
 import Base
 import Text.Megaparsec.Pos (SourcePos (sourceColumn, sourceLine), unPos)
diff --git a/source/Felix/Source.hs b/source/Felix/Source.hs
index 350bb50..68d596c 100644
--- a/source/Felix/Source.hs
+++ b/source/Felix/Source.hs
@@ -80,7 +80,7 @@ import Data.Map.Strict qualified as Map
 import Data.Set qualified as Set
 import Data.Text qualified as Text
 import Data.Text.Encoding qualified as Encoding
-import Report.Location
+import Felix.Report.Location
     ( Location
     , LocationRegistrationError(..)
     , locationToText
diff --git a/source/Felix/Source/Graph.hs b/source/Felix/Source/Graph.hs
index cb8990e..9c8753d 100644
--- a/source/Felix/Source/Graph.hs
+++ b/source/Felix/Source/Graph.hs
@@ -25,11 +25,11 @@ module Felix.Source.Graph
 
 import Base
 import Felix.Source
-import Report.Location
+import Felix.Report.Location
     ( FileId
     , registerFilePathWithDisplay
     )
-import Syntax.Token (Located(..), gatherImports)
+import Felix.Syntax.Token (Located(..), gatherImports)
 
 import Control.Monad (unless)
 import Control.Monad.State.Strict
diff --git a/source/Felix/Store.hs b/source/Felix/Store.hs
index 038b4dc..fb12670 100644
--- a/source/Felix/Store.hs
+++ b/source/Felix/Store.hs
@@ -54,16 +54,16 @@ module Felix.Store
     ) where
 
 import Base
-import Checking.Core
-import Checking.Declaration qualified as Declaration
-import Checking.Identity
-import Checking.Materialization qualified as Materialization
-import Checking.Semantic
+import Felix.Checking.Core
+import Felix.Checking.Declaration qualified as Declaration
+import Felix.Checking.Identity
+import Felix.Checking.Materialization qualified as Materialization
+import Felix.Checking.Semantic
 import Felix.Cache.Codec
 import Felix.Module (ModuleName)
 import Felix.Parsed.Identity qualified as Parsed
 import Felix.Parsed.Payload qualified as ParsedPayload
-import Syntax.Interface qualified as Syntax
+import Felix.Syntax.Interface qualified as Syntax
 
 import Control.Concurrent.MVar
     ( MVar
diff --git a/source/Syntax/Abstract.hs b/source/Felix/Syntax/Abstract.hs
index 76ce6b6..b18612a 100644
--- a/source/Syntax/Abstract.hs
+++ b/source/Felix/Syntax/Abstract.hs
@@ -9,17 +9,17 @@
 -- | Data types for the abstract syntax tree and helper functions
 -- for constructing the lexicon.
 --
-module Syntax.Abstract
-    ( module Syntax.Abstract
-    , module Syntax.LexicalPhrase
-    , module Syntax.Token
+module Felix.Syntax.Abstract
+    ( module Felix.Syntax.Abstract
+    , module Felix.Syntax.LexicalPhrase
+    , module Felix.Syntax.Token
     ) where
 
 
 import Base
-import Syntax.LexicalPhrase (LexicalPhrase, SgPl(..), unsafeReadPhraseSgPl, unsafeReadPhrase)
-import Syntax.Token (Token(..), Located(..))
-import Report.Location
+import Felix.Syntax.LexicalPhrase (LexicalPhrase, SgPl(..), unsafeReadPhraseSgPl, unsafeReadPhrase)
+import Felix.Syntax.Token (Token(..), Located(..))
+import Felix.Report.Location
 
 import Control.DeepSeq (NFData)
 import Text.Earley.Mixfix (Holey)
diff --git a/source/Syntax/Adapt.hs b/source/Felix/Syntax/Adapt.hs
index f496ead..eb0cb6c 100644
--- a/source/Syntax/Adapt.hs
+++ b/source/Felix/Syntax/Adapt.hs
@@ -2,7 +2,7 @@
 {-# LANGUAGE ApplicativeDo #-}
 {-# LANGUAGE RecordWildCards #-}
 
-module Syntax.Adapt
+module Felix.Syntax.Adapt
     ( FunctionPatternError(..)
     , LexicalScanError(..)
     , ScannedLexicalItem(..)
@@ -14,10 +14,10 @@ module Syntax.Adapt
     ) where
 
 import Base
-import Syntax.Abstract
-import Syntax.Interface
-import Syntax.Lexicon
-import Report.Location
+import Felix.Syntax.Abstract
+import Felix.Syntax.Interface
+import Felix.Syntax.Lexicon
+import Felix.Report.Location
 
 import Control.Monad (foldM)
 import Data.Bifunctor qualified as Bifunctor
diff --git a/source/Syntax/Concrete.hs b/source/Felix/Syntax/Concrete.hs
index 62d1f92..8be8ab6 100644
--- a/source/Syntax/Concrete.hs
+++ b/source/Felix/Syntax/Concrete.hs
@@ -3,25 +3,25 @@
 {-# LANGUAGE RecursiveDo #-}
 
 -- | Concrete syntax of the surface language.
-module Syntax.Concrete where
+module Felix.Syntax.Concrete where
 
 import Base
-import Syntax.Abstract
-import Syntax.Concrete.Keywords
-import Syntax.Lexicon
+import Felix.Syntax.Abstract
+import Felix.Syntax.Concrete.Keywords
+import Felix.Syntax.Lexicon
     ( Lexicon(..)
     , SignatureHeadForm(..)
     , concreteSignatureHeadForms
     , lexiconAdjs
     , splitOnVariableSlot
     )
-import Syntax.Token
-import Report.Location
+import Felix.Syntax.Token
+import Felix.Report.Location
 
 import Data.List.NonEmpty qualified as NonEmpty
 import Data.Map.Strict qualified as Map
 import Text.Earley (Grammar, Prod, (<?>), rule, satisfy, terminal)
-import Syntax.Mixfix
+import Felix.Syntax.Mixfix
 
 
 grammar :: Lexicon -> Grammar r (Prod r Text (Located Token) Block)
diff --git a/source/Syntax/Concrete/Keywords.hs b/source/Felix/Syntax/Concrete/Keywords.hs
index a7ac169..eb6d09c 100644
--- a/source/Syntax/Concrete/Keywords.hs
+++ b/source/Felix/Syntax/Concrete/Keywords.hs
@@ -18,12 +18,12 @@ The names are chosen using the following criteria:
 This module also defines symbols that have special uses
 (such as @_colon@ for its use in type signatures).
 -}
-module Syntax.Concrete.Keywords where
+module Felix.Syntax.Concrete.Keywords where
 
 
 import Base
-import Syntax.Token
-import Report.Location
+import Felix.Syntax.Token
+import Felix.Report.Location
 
 import Text.Earley (Prod, (<?>), terminal)
 
diff --git a/source/Syntax/Interface.hs b/source/Felix/Syntax/Interface.hs
index 4b84cec..1820705 100644
--- a/source/Syntax/Interface.hs
+++ b/source/Felix/Syntax/Interface.hs
@@ -2,7 +2,7 @@
 {-# LANGUAGE DerivingStrategies #-}
 {-# LANGUAGE NoImplicitPrelude #-}
 
-module Syntax.Interface
+module Felix.Syntax.Interface
     ( MixfixLevel
     , mixfixLevel
     , mixfixLevelValue
@@ -56,9 +56,9 @@ module Syntax.Interface
 import Base
 
 import Felix.Cache.Codec
-import Syntax.Abstract
-import Syntax.Lexicon
-import Syntax.Pragma
+import Felix.Syntax.Abstract
+import Felix.Syntax.Lexicon
+import Felix.Syntax.Pragma
 
 import Control.DeepSeq (NFData)
 import Control.Monad (unless)
diff --git a/source/Syntax/Internal.hs b/source/Felix/Syntax/Internal.hs
index 5a8cb65..d129947 100644
--- a/source/Syntax/Internal.hs
+++ b/source/Felix/Syntax/Internal.hs
@@ -6,25 +6,25 @@
 {-# LANGUAGE ViewPatterns #-}
 
 -- | Data types for the internal (semantic) syntax tree.
-module Syntax.Internal
-    ( module Syntax.Internal
-    , module Syntax.Abstract
-    , module Syntax.LexicalPhrase
-    , module Syntax.Token
+module Felix.Syntax.Internal
+    ( module Felix.Syntax.Internal
+    , module Felix.Syntax.Abstract
+    , module Felix.Syntax.LexicalPhrase
+    , module Felix.Syntax.Token
     ) where
 
 
 import Base
-import Syntax.Lexicon
+import Felix.Syntax.Lexicon
     ( pattern PairSymbol
     , pattern UnionsSymbol
     , pattern UpairSymbol
     )
-import Syntax.LexicalPhrase (unsafeReadPhrase, unsafeReadPhraseSgPl)
-import Syntax.Token (Token(..))
-import Report.Location
+import Felix.Syntax.LexicalPhrase (unsafeReadPhrase, unsafeReadPhraseSgPl)
+import Felix.Syntax.Token (Token(..))
+import Felix.Report.Location
 
-import Syntax.Abstract
+import Felix.Syntax.Abstract
     ( Chain(..)
     , Associativity(..)
     , Connective(..)
diff --git a/source/Syntax/LexicalPhrase.hs b/source/Felix/Syntax/LexicalPhrase.hs
index a0e0f19..5eb5b18 100644
--- a/source/Syntax/LexicalPhrase.hs
+++ b/source/Felix/Syntax/LexicalPhrase.hs
@@ -1,11 +1,11 @@
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE NoImplicitPrelude #-}
 
-module Syntax.LexicalPhrase where
+module Felix.Syntax.LexicalPhrase where
 
 
 import Base
-import Syntax.Token (Token(..))
+import Felix.Syntax.Token (Token(..))
 
 import Control.DeepSeq (NFData)
 import Data.Char (isAlpha)
diff --git a/source/Syntax/Lexicon.hs b/source/Felix/Syntax/Lexicon.hs
index 3e815c7..c3332c7 100644
--- a/source/Syntax/Lexicon.hs
+++ b/source/Felix/Syntax/Lexicon.hs
@@ -9,8 +9,8 @@
 -- extension easier.
 --
 
-module Syntax.Lexicon
-    ( module Syntax.Lexicon
+module Felix.Syntax.Lexicon
+    ( module Felix.Syntax.Lexicon
     , pattern ConsSymbol
     , pattern PairSymbol
     , pattern UpairSymbol
@@ -22,14 +22,14 @@ module Syntax.Lexicon
 
 
 import Base
-import Syntax.Abstract
+import Felix.Syntax.Abstract
 
 import Data.List qualified as List
 import Data.Sequence qualified as Seq
 import Data.Set qualified as Set
 import Data.Map.Strict qualified as Map
 import Data.Text qualified as Text
-import Syntax.Mixfix (Holey)
+import Felix.Syntax.Mixfix (Holey)
 
 
 data SignatureHeadForm
diff --git a/source/Syntax/Mixfix.hs b/source/Felix/Syntax/Mixfix.hs
index 6489d46..a3ce4bb 100644
--- a/source/Syntax/Mixfix.hs
+++ b/source/Felix/Syntax/Mixfix.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE RecursiveDo #-}
 
-module Syntax.Mixfix where
+module Felix.Syntax.Mixfix where
 
 {-
 Original code Copyright (c) 2014-2019, Olle Fredriksson
@@ -39,7 +39,7 @@ OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 import Base
 import Text.Earley
 import Data.Either
-import Syntax.Abstract
+import Felix.Syntax.Abstract
 
 
 replicateA :: Applicative f => Int -> f a -> f [a]
diff --git a/source/Syntax/Pragma.hs b/source/Felix/Syntax/Pragma.hs
index 94c0d46..97d1482 100644
--- a/source/Syntax/Pragma.hs
+++ b/source/Felix/Syntax/Pragma.hs
@@ -2,7 +2,7 @@
 {-# LANGUAGE DerivingStrategies #-}
 {-# LANGUAGE NoImplicitPrelude #-}
 
-module Syntax.Pragma
+module Felix.Syntax.Pragma
     ( SourceMixfixLevel
     , sourceMixfixLevelValue
     , SyntaxPragma(..)
@@ -14,8 +14,8 @@ module Syntax.Pragma
 
 import Base
 
-import Report.Location
-import Syntax.Abstract (Associativity(..))
+import Felix.Report.Location
+import Felix.Syntax.Abstract (Associativity(..))
 
 import Control.DeepSeq (NFData)
 import Control.Monad (unless, when)
diff --git a/source/Syntax/Token.hs b/source/Felix/Syntax/Token.hs
index b16379b..31d1d19 100644
--- a/source/Syntax/Token.hs
+++ b/source/Felix/Syntax/Token.hs
@@ -13,7 +13,7 @@
 -- (α, β, γ, ..., 𝔸, 𝔹, ℂ, ...). Similarly, @\\begin{...}@ and @\\end{...}@ commands
 -- are each parsed as single tokens.
 --
-module Syntax.Token
+module Felix.Syntax.Token
     ( Token(..)
     , VariableDisplay(..)
     , VariableSuffix(..)
@@ -30,7 +30,7 @@ module Syntax.Token
 
 import Base hiding (many)
 
-import Report.Location
+import Felix.Report.Location
 
 import Control.DeepSeq (NFData)
 import Control.Monad.Combinators
diff --git a/source/Test/All.hs b/source/Felix/Test/All.hs
index 7fb5bd3..7cdc49c 100644
--- a/source/Test/All.hs
+++ b/source/Felix/Test/All.hs
@@ -1,9 +1,9 @@
-module Test.All where
+module Felix.Test.All where
 
 
 import Base
-import Test.Golden
-import Test.Unit
+import Felix.Test.Golden
+import Felix.Test.Unit
 import Test.Tasty
 
 
diff --git a/source/Test/Golden.hs b/source/Felix/Test/Golden.hs
index c700d06..905ff73 100644
--- a/source/Test/Golden.hs
+++ b/source/Felix/Test/Golden.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 {-# LANGUAGE RecordWildCards #-}
 
-module Test.Golden where
+module Felix.Test.Golden where
 
 
 import Base
diff --git a/source/Felix/Test/Unit.hs b/source/Felix/Test/Unit.hs
new file mode 100644
index 0000000..f11d21f
--- /dev/null
+++ b/source/Felix/Test/Unit.hs
@@ -0,0 +1,52 @@
+module Felix.Test.Unit where
+
+
+import Felix.Test.Unit.Abstract qualified as Abstract
+import Felix.Test.Unit.Backend qualified as Backend
+import Felix.Test.Unit.CommandLine qualified as CommandLine
+import Felix.Test.Unit.Concrete qualified as Concrete
+import Felix.Test.Unit.Core qualified as Core
+import Felix.Test.Unit.Declaration qualified as Declaration
+import Felix.Test.Unit.Foundation qualified as Foundation
+import Felix.Test.Unit.Html qualified as Html
+import Felix.Test.Unit.HtmlLayout qualified as HtmlLayout
+import Felix.Test.Unit.HtmlOutput qualified as HtmlOutput
+import Felix.Test.Unit.Identity qualified as Identity
+import Felix.Test.Unit.Kernel qualified as Kernel
+import Felix.Test.Unit.Lexicon qualified as Lexicon
+import Felix.Test.Unit.Materialization qualified as Materialization
+import Felix.Test.Unit.Meaning qualified as Meaning
+import Felix.Test.Unit.Module qualified as Module
+import Felix.Test.Unit.OutputPlan qualified as OutputPlan
+import Felix.Test.Unit.Provers qualified as Provers
+import Felix.Test.Unit.Semantic qualified as Semantic
+import Felix.Test.Unit.Source qualified as Source
+import Felix.Test.Unit.Store qualified as Store
+import Felix.Test.Unit.Token qualified as Token
+import Test.Tasty
+
+unitTests :: TestTree
+unitTests = testGroup "unit tests"
+    [ Abstract.unitTests
+    , Backend.unitTests
+    , CommandLine.unitTests
+    , Concrete.unitTests
+    , Core.unitTests
+    , Declaration.unitTests
+    , Foundation.unitTests
+    , Identity.unitTests
+    , Html.unitTests
+    , HtmlLayout.unitTests
+    , HtmlOutput.unitTests
+    , Kernel.unitTests
+    , Lexicon.unitTests
+    , Meaning.unitTests
+    , Materialization.unitTests
+    , Module.unitTests
+    , OutputPlan.unitTests
+    , Provers.unitTests
+    , Semantic.unitTests
+    , Source.unitTests
+    , Store.unitTests
+    , Token.unitTests
+    ]
diff --git a/source/Test/Unit/Abstract.hs b/source/Felix/Test/Unit/Abstract.hs
index 61118bd..c487c2a 100644
--- a/source/Test/Unit/Abstract.hs
+++ b/source/Felix/Test/Unit/Abstract.hs
@@ -1,10 +1,10 @@
 {-# LANGUAGE OverloadedStrings #-}
 
-module Test.Unit.Abstract (unitTests) where
+module Felix.Test.Unit.Abstract (unitTests) where
 
 import Base
-import Report.Location
-import Syntax.Abstract
+import Felix.Report.Location
+import Felix.Syntax.Abstract
 
 import Hedgehog
 import Hedgehog.Gen qualified as Gen
diff --git a/source/Test/Unit/Backend.hs b/source/Felix/Test/Unit/Backend.hs
index 5243c96..384d21b 100644
--- a/source/Test/Unit/Backend.hs
+++ b/source/Felix/Test/Unit/Backend.hs
@@ -1,13 +1,13 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 {-# LANGUAGE OverloadedStrings #-}
 
-module Test.Unit.Backend (unitTests) where
+module Felix.Test.Unit.Backend (unitTests) where
 
 import Base hiding (Empty)
-import Checking.Backend.Problem
-import Checking.Backend.Tptp
-import Checking.Core
-import Checking.Foundation qualified as Foundation
+import Felix.Checking.Backend.Problem
+import Felix.Checking.Backend.Tptp
+import Felix.Checking.Core
+import Felix.Checking.Foundation qualified as Foundation
 import Felix.Provers
 import Tptp.UnsortedFirstOrder qualified as Tptp
 
diff --git a/source/Test/Unit/CommandLine.hs b/source/Felix/Test/Unit/CommandLine.hs
index 110e00d..f2a4a10 100644
--- a/source/Test/Unit/CommandLine.hs
+++ b/source/Felix/Test/Unit/CommandLine.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE OverloadedStrings #-}
 
-module Test.Unit.CommandLine (unitTests) where
+module Felix.Test.Unit.CommandLine (unitTests) where
 
 import Base
 import Felix.CommandLine
@@ -9,8 +9,8 @@ import Felix.Source (safeRelativePath)
 import Felix.Store qualified as Store
 import Felix.Verification qualified as Verification
 import Felix.Provers qualified as Provers
-import Render.Html.Output qualified as HtmlOutput
-import Report.Location (pattern Nowhere)
+import Felix.Render.Html.Output qualified as HtmlOutput
+import Felix.Report.Location (pattern Nowhere)
 
 import Control.Exception (IOException, bracket)
 import Control.Exception qualified as Exception
diff --git a/source/Test/Unit/Concrete.hs b/source/Felix/Test/Unit/Concrete.hs
index 7776552..7eac7df 100644
--- a/source/Test/Unit/Concrete.hs
+++ b/source/Felix/Test/Unit/Concrete.hs
@@ -1,13 +1,13 @@
 {-# LANGUAGE OverloadedStrings #-}
 
-module Test.Unit.Concrete (unitTests) where
+module Felix.Test.Unit.Concrete (unitTests) where
 
 import Base
-import Report.Location
-import Syntax.Abstract qualified as Raw
-import Syntax.Concrete (grammar)
-import Syntax.Lexicon (builtins)
-import Syntax.Token (runLexer)
+import Felix.Report.Location
+import Felix.Syntax.Abstract qualified as Raw
+import Felix.Syntax.Concrete (grammar)
+import Felix.Syntax.Lexicon (builtins)
+import Felix.Syntax.Token (runLexer)
 
 import Data.Text qualified as Text
 import Test.Tasty
diff --git a/source/Test/Unit/Core.hs b/source/Felix/Test/Unit/Core.hs
index 643dc38..0388c7f 100644
--- a/source/Test/Unit/Core.hs
+++ b/source/Felix/Test/Unit/Core.hs
@@ -1,11 +1,11 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
-module Test.Unit.Core (unitTests) where
+module Felix.Test.Unit.Core (unitTests) where
 
 import Base hiding (Empty)
-import Checking.Core
-import Checking.Foundation qualified as Foundation
-import Checking.SetConstruction
+import Felix.Checking.Core
+import Felix.Checking.Foundation qualified as Foundation
+import Felix.Checking.SetConstruction
 
 import Control.DeepSeq (NFData(..), force)
 import Hedgehog
diff --git a/source/Test/Unit/Declaration.hs b/source/Felix/Test/Unit/Declaration.hs
index 32d979c..f3d9be7 100644
--- a/source/Test/Unit/Declaration.hs
+++ b/source/Felix/Test/Unit/Declaration.hs
@@ -1,31 +1,31 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
-module Test.Unit.Declaration (unitTests) where
+module Felix.Test.Unit.Declaration (unitTests) where
 
 import Base
-import Checking.Authority qualified as Authority
-import Checking.Backend.Problem qualified as Backend
-import Checking.Core qualified as Core
-import Checking.Declaration qualified as Declaration
-import Checking.Foundation qualified as Foundation
-import Checking.Exact qualified as Exact
-import Checking.Exact.Vocabulary qualified as Vocabulary
-import Checking.Identity qualified as Identity
-import Checking.Kernel.Derivation qualified as Kernel
-import Checking.SetConstruction qualified as SetConstruction
-import Checking.Semantic qualified as Semantic
-import Checking.Typed.Inductive qualified as Typed
+import Felix.Checking.Authority qualified as Authority
+import Felix.Checking.Backend.Problem qualified as Backend
+import Felix.Checking.Core qualified as Core
+import Felix.Checking.Declaration qualified as Declaration
+import Felix.Checking.Foundation qualified as Foundation
+import Felix.Checking.Exact qualified as Exact
+import Felix.Checking.Exact.Vocabulary qualified as Vocabulary
+import Felix.Checking.Identity qualified as Identity
+import Felix.Checking.Kernel.Derivation qualified as Kernel
+import Felix.Checking.SetConstruction qualified as SetConstruction
+import Felix.Checking.Semantic qualified as Semantic
+import Felix.Checking.Typed.Inductive qualified as Typed
 import Felix.Math.Codec
 import Felix.Module
 import Felix.Source
 import Felix.Store qualified as Store
 import Felix.Meaning qualified as Meaning
 import Felix.Provers qualified as Provers
-import Report.Location
-import Syntax.Abstract qualified as Raw
-import Syntax.Interface qualified as Syntax
-import Syntax.Internal qualified as Internal
-import Syntax.Lexicon qualified as Lexicon
+import Felix.Report.Location
+import Felix.Syntax.Abstract qualified as Raw
+import Felix.Syntax.Interface qualified as Syntax
+import Felix.Syntax.Internal qualified as Internal
+import Felix.Syntax.Lexicon qualified as Lexicon
 
 import Data.List.NonEmpty qualified as NonEmpty
 import Data.IORef qualified as IORef
diff --git a/source/Test/Unit/Foundation.hs b/source/Felix/Test/Unit/Foundation.hs
index 17ff526..18ead04 100644
--- a/source/Test/Unit/Foundation.hs
+++ b/source/Felix/Test/Unit/Foundation.hs
@@ -1,10 +1,10 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
-module Test.Unit.Foundation (unitTests) where
+module Felix.Test.Unit.Foundation (unitTests) where
 
 import Base
-import Checking.Core
-import Checking.Foundation
+import Felix.Checking.Core
+import Felix.Checking.Foundation
 
 import Data.List qualified as List
 import Data.Set qualified as Set
diff --git a/source/Test/Unit/Html.hs b/source/Felix/Test/Unit/Html.hs
index c7f24c4..c8395ec 100644
--- a/source/Test/Unit/Html.hs
+++ b/source/Felix/Test/Unit/Html.hs
@@ -1,17 +1,17 @@
 {-# LANGUAGE OverloadedStrings #-}
 
-module Test.Unit.Html (unitTests) where
+module Felix.Test.Unit.Html (unitTests) where
 
 import Base
 import Felix.Parse qualified as Parse
 import Felix.Source
 import Felix.Source.Graph
 import Felix.Workspace qualified as Workspace
-import Render.Html qualified as Html
-import Render.Html.Context
-import Render.Html.Layout
-import Report.Location (Location, pattern Nowhere)
-import Syntax.Abstract
+import Felix.Render.Html qualified as Html
+import Felix.Render.Html.Context
+import Felix.Render.Html.Layout
+import Felix.Report.Location (Location, pattern Nowhere)
+import Felix.Syntax.Abstract
 
 import Data.Text qualified as Text
 import Data.Text.IO qualified as TextIO
diff --git a/source/Test/Unit/HtmlLayout.hs b/source/Felix/Test/Unit/HtmlLayout.hs
index a248f3b..a3d701f 100644
--- a/source/Test/Unit/HtmlLayout.hs
+++ b/source/Felix/Test/Unit/HtmlLayout.hs
@@ -1,11 +1,11 @@
 {-# LANGUAGE OverloadedStrings #-}
 
-module Test.Unit.HtmlLayout (unitTests) where
+module Felix.Test.Unit.HtmlLayout (unitTests) where
 
 import Base
 import Felix.Source
 import Felix.Source.Graph
-import Render.Html.Layout
+import Felix.Render.Html.Layout
 
 import Control.Exception (bracket)
 import Data.List qualified as List
diff --git a/source/Test/Unit/HtmlOutput.hs b/source/Felix/Test/Unit/HtmlOutput.hs
index 0087f82..34fe2e7 100644
--- a/source/Test/Unit/HtmlOutput.hs
+++ b/source/Felix/Test/Unit/HtmlOutput.hs
@@ -1,15 +1,15 @@
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE OverloadedStrings #-}
 
-module Test.Unit.HtmlOutput (unitTests) where
+module Felix.Test.Unit.HtmlOutput (unitTests) where
 
 import Base
 import Felix.Parse qualified as Parse
 import Felix.Source
 import Felix.Source.Graph qualified as SourceGraph
-import Render.Html qualified as Html
-import Render.Html.Export
-import Render.Html.Output
+import Felix.Render.Html qualified as Html
+import Felix.Render.Html.Export
+import Felix.Render.Html.Output
 
 import Control.Exception (bracket)
 import Data.ByteString qualified as ByteString
diff --git a/source/Test/Unit/Identity.hs b/source/Felix/Test/Unit/Identity.hs
index 0cb46a5..7e1e73f 100644
--- a/source/Test/Unit/Identity.hs
+++ b/source/Felix/Test/Unit/Identity.hs
@@ -1,12 +1,12 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
-module Test.Unit.Identity (unitTests) where
+module Felix.Test.Unit.Identity (unitTests) where
 
 import Base
-import Checking.Authority qualified as Authority
-import Checking.Core qualified as Core
-import Checking.Foundation qualified as Foundation
-import Checking.Identity qualified as Identity
+import Felix.Checking.Authority qualified as Authority
+import Felix.Checking.Core qualified as Core
+import Felix.Checking.Foundation qualified as Foundation
+import Felix.Checking.Identity qualified as Identity
 import Felix.Cache.Codec
 import Felix.Math.Codec
 import Felix.Module
diff --git a/source/Test/Unit/Kernel.hs b/source/Felix/Test/Unit/Kernel.hs
index d01a194..7762a7e 100644
--- a/source/Test/Unit/Kernel.hs
+++ b/source/Felix/Test/Unit/Kernel.hs
@@ -1,17 +1,17 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 {-# LANGUAGE PatternSynonyms #-}
 
-module Test.Unit.Kernel (unitTests) where
+module Felix.Test.Unit.Kernel (unitTests) where
 
 import Base hiding (Empty)
-import Checking.Core
-import Checking.Foundation qualified as Foundation
-import Checking.Kernel.Derivation
-import Checking.Kernel.Semantics qualified as Semantics
-import Checking.Kernel.SetLfp qualified as SetLfp
-import Checking.Typed.Inductive qualified as Inductive
-import Report.Location (pattern Nowhere)
-import Syntax.Internal qualified as Internal
+import Felix.Checking.Core
+import Felix.Checking.Foundation qualified as Foundation
+import Felix.Checking.Kernel.Derivation
+import Felix.Checking.Kernel.Semantics qualified as Semantics
+import Felix.Checking.Kernel.SetLfp qualified as SetLfp
+import Felix.Checking.Typed.Inductive qualified as Inductive
+import Felix.Report.Location (pattern Nowhere)
+import Felix.Syntax.Internal qualified as Internal
 
 import Data.Set qualified as Set
 import Data.Vector qualified as Vector
diff --git a/source/Test/Unit/Lexicon.hs b/source/Felix/Test/Unit/Lexicon.hs
index 54b4bd4..4b7f9e7 100644
--- a/source/Test/Unit/Lexicon.hs
+++ b/source/Felix/Test/Unit/Lexicon.hs
@@ -1,12 +1,12 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
-module Test.Unit.Lexicon (unitTests) where
+module Felix.Test.Unit.Lexicon (unitTests) where
 
 import Base
 import Felix.Cache.Codec
-import Syntax.Abstract
-import Syntax.Interface
-import Syntax.Lexicon
+import Felix.Syntax.Abstract
+import Felix.Syntax.Interface
+import Felix.Syntax.Lexicon
 
 import Data.Set qualified as Set
 import Test.Tasty
diff --git a/source/Test/Unit/Materialization.hs b/source/Felix/Test/Unit/Materialization.hs
index fcad7b5..9c4f54f 100644
--- a/source/Test/Unit/Materialization.hs
+++ b/source/Felix/Test/Unit/Materialization.hs
@@ -1,14 +1,14 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
-module Test.Unit.Materialization (unitTests) where
+module Felix.Test.Unit.Materialization (unitTests) where
 
 import Base
-import Checking.Authority qualified as Authority
-import Checking.Core qualified as Core
-import Checking.Foundation qualified as Foundation
-import Checking.Identity qualified as Identity
-import Checking.Materialization qualified as Materialization
-import Checking.Semantic qualified as Semantic
+import Felix.Checking.Authority qualified as Authority
+import Felix.Checking.Core qualified as Core
+import Felix.Checking.Foundation qualified as Foundation
+import Felix.Checking.Identity qualified as Identity
+import Felix.Checking.Materialization qualified as Materialization
+import Felix.Checking.Semantic qualified as Semantic
 import Felix.Math.Codec
 import Felix.Module
 import Felix.Source
diff --git a/source/Test/Unit/Meaning.hs b/source/Felix/Test/Unit/Meaning.hs
index acb33d0..3093a84 100644
--- a/source/Test/Unit/Meaning.hs
+++ b/source/Felix/Test/Unit/Meaning.hs
@@ -1,13 +1,13 @@
 {-# LANGUAGE OverloadedStrings #-}
 
-module Test.Unit.Meaning (unitTests) where
+module Felix.Test.Unit.Meaning (unitTests) where
 
 import Base
 import Felix.Meaning
-import Report.Location
-import Syntax.Abstract qualified as Raw
-import Syntax.Internal qualified as Sem
-import Syntax.LexicalPhrase
+import Felix.Report.Location
+import Felix.Syntax.Abstract qualified as Raw
+import Felix.Syntax.Internal qualified as Sem
+import Felix.Syntax.LexicalPhrase
     ( unsafeReadPhrase
     , unsafeReadPhraseSgPl
     )
diff --git a/source/Test/Unit/Module.hs b/source/Felix/Test/Unit/Module.hs
index 13fe90d..44f0ccb 100644
--- a/source/Test/Unit/Module.hs
+++ b/source/Felix/Test/Unit/Module.hs
@@ -1,40 +1,40 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
-module Test.Unit.Module (unitTests) where
+module Felix.Test.Unit.Module (unitTests) where
 
 import Base
-import Checking.Authority qualified as Authority
-import Checking.Backend.Problem qualified as Backend
-import Checking.Core qualified as Core
-import Checking.Declaration qualified as Declaration
-import Checking.Exact qualified as Exact
-import Checking.Exact.Datatype qualified as ExactDatatype
-import Checking.Exact.Inductive qualified as ExactInductive
-import Checking.Exact.Proof qualified as ExactProof
-import Checking.FinalPrelude qualified as FinalPrelude
-import Checking.Foundation qualified as Foundation
-import Checking.Identity qualified as Identity
-import Checking.Module qualified as Module
-import Checking.Semantic qualified as Semantic
-import Checking.Typed.Inductive qualified as TypedInductive
+import Felix.Checking.Authority qualified as Authority
+import Felix.Checking.Backend.Problem qualified as Backend
+import Felix.Checking.Core qualified as Core
+import Felix.Checking.Declaration qualified as Declaration
+import Felix.Checking.Exact qualified as Exact
+import Felix.Checking.Exact.Datatype qualified as ExactDatatype
+import Felix.Checking.Exact.Inductive qualified as ExactInductive
+import Felix.Checking.Exact.Proof qualified as ExactProof
+import Felix.Checking.FinalPrelude qualified as FinalPrelude
+import Felix.Checking.Foundation qualified as Foundation
+import Felix.Checking.Identity qualified as Identity
+import Felix.Checking.Module qualified as Module
+import Felix.Checking.Semantic qualified as Semantic
+import Felix.Checking.Typed.Inductive qualified as TypedInductive
 import Felix.CommandLine qualified as CommandLine
-import Felix.Module
 import Felix.Math.Codec
+import Felix.Module
 import Felix.Parse qualified as Parse
 import Felix.Prelude qualified as Prelude
+import Felix.Provers qualified as Provers
+import Felix.Report.Location
 import Felix.Source
 import Felix.Source.Content qualified as Content
 import Felix.Store qualified as Store
+import Felix.Syntax.Abstract qualified as Raw
+import Felix.Syntax.Interface qualified as Syntax
+import Felix.Syntax.Internal qualified as Internal
+import Felix.Syntax.Lexicon qualified as Lexicon
+import Felix.Syntax.Pragma qualified as Pragma
 import Felix.Verification qualified as Verification
 import Felix.Workspace qualified as Workspace
-import Report.Location
-import Felix.Provers qualified as Provers
 import Paths_felix qualified as Paths
-import Syntax.Abstract qualified as Raw
-import Syntax.Internal qualified as Internal
-import Syntax.Interface qualified as Syntax
-import Syntax.Lexicon qualified as Lexicon
-import Syntax.Pragma qualified as Pragma
 
 import Control.Concurrent (threadDelay)
 import Control.Concurrent.STM
diff --git a/source/Test/Unit/OutputPlan.hs b/source/Felix/Test/Unit/OutputPlan.hs
index 45658bf..803b7da 100644
--- a/source/Test/Unit/OutputPlan.hs
+++ b/source/Felix/Test/Unit/OutputPlan.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
-module Test.Unit.OutputPlan (unitTests) where
+module Felix.Test.Unit.OutputPlan (unitTests) where
 
 import Base
 import Felix.OutputPlan qualified as Output
diff --git a/source/Test/Unit/Provers.hs b/source/Felix/Test/Unit/Provers.hs
index 0d0cf1b..f1e3cc1 100644
--- a/source/Test/Unit/Provers.hs
+++ b/source/Felix/Test/Unit/Provers.hs
@@ -1,10 +1,10 @@
 {-# LANGUAGE OverloadedStrings #-}
 
-module Test.Unit.Provers (unitTests) where
+module Felix.Test.Unit.Provers (unitTests) where
 
 import Base hiding (Empty)
-import Checking.Backend.Problem
-import Checking.Core
+import Felix.Checking.Backend.Problem
+import Felix.Checking.Core
 import Felix.Provers
 
 import Control.Concurrent
@@ -26,7 +26,7 @@ import Data.Set qualified as Set
 import Data.Text qualified as Text
 import Data.Text.IO qualified as Text
 import Data.Vector qualified as Vector
-import Report.Location (Location(..))
+import Felix.Report.Location (Location(..))
 import System.Directory qualified as Directory
 import System.Exit (ExitCode(..))
 import System.FilePath.Posix ((</>))
diff --git a/source/Test/Unit/Semantic.hs b/source/Felix/Test/Unit/Semantic.hs
index 160735c..f62a003 100644
--- a/source/Test/Unit/Semantic.hs
+++ b/source/Felix/Test/Unit/Semantic.hs
@@ -1,21 +1,21 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
-module Test.Unit.Semantic (unitTests) where
+module Felix.Test.Unit.Semantic (unitTests) where
 
 import Base
-import Checking.Authority qualified as Authority
-import Checking.Core qualified as Core
-import Checking.Foundation qualified as Foundation
-import Checking.Identity qualified as Identity
-import Checking.Semantic qualified as Semantic
+import Felix.Checking.Authority qualified as Authority
+import Felix.Checking.Core qualified as Core
+import Felix.Checking.Foundation qualified as Foundation
+import Felix.Checking.Identity qualified as Identity
+import Felix.Checking.Semantic qualified as Semantic
 import Felix.Cache.Codec
 import Felix.Math.Codec
 import Felix.Module
 import Felix.Parsed.Identity
 import Felix.Source
 import Felix.Source.Content
-import Syntax.Interface qualified as Syntax
-import Syntax.Abstract qualified as Raw
+import Felix.Syntax.Interface qualified as Syntax
+import Felix.Syntax.Abstract qualified as Raw
 
 import Data.ByteString (ByteString)
 import Data.List qualified as List
diff --git a/source/Test/Unit/Source.hs b/source/Felix/Test/Unit/Source.hs
index a8e4506..6216381 100644
--- a/source/Test/Unit/Source.hs
+++ b/source/Felix/Test/Unit/Source.hs
@@ -2,12 +2,12 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PatternSynonyms #-}
 
-module Test.Unit.Source (unitTests) where
+module Felix.Test.Unit.Source (unitTests) where
 
 import Base
-import Checking.Foundation qualified as Foundation
-import Checking.Identity qualified as Identity
-import Checking.Semantic qualified as Semantic
+import Felix.Checking.Foundation qualified as Foundation
+import Felix.Checking.Identity qualified as Identity
+import Felix.Checking.Semantic qualified as Semantic
 import Felix.Cache.Codec qualified as Cache
 import Felix.Module qualified as Module
 import Felix.Parse qualified as Parse
@@ -18,7 +18,7 @@ import Felix.Source
 import Felix.Source.Content qualified as Content
 import Felix.Source.Graph
 import Felix.Store qualified as Store
-import Report.Location
+import Felix.Report.Location
     ( FileId(..)
     , FileIdAllocator(..)
     , Location(..)
@@ -30,10 +30,10 @@ import Report.Location
     , locLine
     , lookupFileIdentityPath
     )
-import Syntax.Abstract qualified as Raw
-import Syntax.Adapt qualified as Adapt
-import Syntax.Interface qualified as Interface
-import Syntax.Token (runLexer)
+import Felix.Syntax.Abstract qualified as Raw
+import Felix.Syntax.Adapt qualified as Adapt
+import Felix.Syntax.Interface qualified as Interface
+import Felix.Syntax.Token (runLexer)
 
 import Control.Exception (bracket, evaluate)
 import Data.ByteString qualified as ByteString
diff --git a/source/Test/Unit/Store.hs b/source/Felix/Test/Unit/Store.hs
index fb207d1..423204c 100644
--- a/source/Test/Unit/Store.hs
+++ b/source/Felix/Test/Unit/Store.hs
@@ -1,15 +1,15 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
-module Test.Unit.Store (unitTests) where
+module Felix.Test.Unit.Store (unitTests) where
 
 import Base
-import Checking.Authority qualified as Authority
-import Checking.Core qualified as Core
-import Checking.Declaration qualified as Declaration
-import Checking.Foundation qualified as Foundation
-import Checking.Identity qualified as Identity
-import Checking.Module qualified as Typed
-import Checking.Semantic qualified as Semantic
+import Felix.Checking.Authority qualified as Authority
+import Felix.Checking.Core qualified as Core
+import Felix.Checking.Declaration qualified as Declaration
+import Felix.Checking.Foundation qualified as Foundation
+import Felix.Checking.Identity qualified as Identity
+import Felix.Checking.Module qualified as Typed
+import Felix.Checking.Semantic qualified as Semantic
 import Felix.Cache.Codec qualified as Cache
 import Felix.Math.Codec
 import Felix.Module
@@ -19,7 +19,7 @@ import Felix.Source.Content qualified as Content
 import Felix.Source
 import Felix.Store qualified as Store
 import Felix.Provers qualified as Provers
-import Syntax.Interface qualified as Syntax
+import Felix.Syntax.Interface qualified as Syntax
 
 import Control.Concurrent (threadDelay)
 import Control.Exception qualified as Exception
diff --git a/source/Test/Unit/Token.hs b/source/Felix/Test/Unit/Token.hs
index d399e2a..00c6755 100644
--- a/source/Test/Unit/Token.hs
+++ b/source/Felix/Test/Unit/Token.hs
@@ -1,14 +1,14 @@
 {-# LANGUAGE OverloadedStrings #-}
 
-module Test.Unit.Token (unitTests) where
+module Felix.Test.Unit.Token (unitTests) where
 
 import Base
-import Report.Location
-import Syntax.Adapt
-import Syntax.Abstract (Associativity(..))
-import Syntax.Interface
-import Syntax.Pragma
-import Syntax.Token
+import Felix.Report.Location
+import Felix.Syntax.Adapt
+import Felix.Syntax.Abstract (Associativity(..))
+import Felix.Syntax.Interface
+import Felix.Syntax.Pragma
+import Felix.Syntax.Token
 
 import Data.Text qualified as Text
 import Test.Tasty
diff --git a/source/Felix/Verification.hs b/source/Felix/Verification.hs
index 572f3ce..716beea 100644
--- a/source/Felix/Verification.hs
+++ b/source/Felix/Verification.hs
@@ -48,11 +48,11 @@ module Felix.Verification
 
 
 import Base
-import Checking.Declaration qualified as Declaration
-import Checking.Foundation qualified as Foundation
-import Checking.Identity qualified as Identity
-import Checking.Module qualified as Typed
-import Checking.Semantic qualified as Semantic
+import Felix.Checking.Declaration qualified as Declaration
+import Felix.Checking.Foundation qualified as Foundation
+import Felix.Checking.Identity qualified as Identity
+import Felix.Checking.Module qualified as Typed
+import Felix.Checking.Semantic qualified as Semantic
 import Felix.Module (localDeclarationOrdinal)
 import Felix.Parse (ParseWorkspaceError(..), ParsedSourceWorkspace)
 import Felix.Parse qualified as Felix
@@ -61,10 +61,10 @@ import Felix.Provers
 import Felix.Source
 import Felix.Source.Graph (ResolvedSourceGraph)
 import Felix.Store qualified as Store
-import Render.Html.Export qualified as HtmlExport
-import Report.Location
-import Syntax.Abstract qualified as Raw
-import Syntax.Interface qualified as Syntax
+import Felix.Render.Html.Export qualified as HtmlExport
+import Felix.Report.Location
+import Felix.Syntax.Abstract qualified as Raw
+import Felix.Syntax.Interface qualified as Syntax
 
 import Control.Exception qualified as Exception
 import Control.Monad (unless)
diff --git a/source/Felix/Workspace.hs b/source/Felix/Workspace.hs
index 6a13d42..b9034c5 100644
--- a/source/Felix/Workspace.hs
+++ b/source/Felix/Workspace.hs
@@ -29,11 +29,11 @@ import Felix.Prelude qualified as Prelude
 import Felix.Source
 import Felix.Source.Graph (ResolvedSourceGraph)
 import Felix.Source.Graph qualified as SourceGraph
-import Report.Location
-import Syntax.Abstract qualified as Raw
-import Syntax.Adapt (ScannedLexicalItem, scanChunk)
-import Syntax.Lexicon (builtins)
-import Syntax.Token
+import Felix.Report.Location
+import Felix.Syntax.Abstract qualified as Raw
+import Felix.Syntax.Adapt (ScannedLexicalItem, scanChunk)
+import Felix.Syntax.Lexicon (builtins)
+import Felix.Syntax.Token
 
 import Control.Exception qualified as Exception
 import Data.Bifunctor (first)
diff --git a/source/Test/Unit.hs b/source/Test/Unit.hs
deleted file mode 100644
index 3e5817c..0000000
--- a/source/Test/Unit.hs
+++ /dev/null
@@ -1,52 +0,0 @@
-module Test.Unit where
-
-
-import Test.Tasty
-import Test.Unit.Abstract qualified as Abstract
-import Test.Unit.Backend qualified as Backend
-import Test.Unit.CommandLine qualified as CommandLine
-import Test.Unit.Concrete qualified as Concrete
-import Test.Unit.Core qualified as Core
-import Test.Unit.Declaration qualified as Declaration
-import Test.Unit.Foundation qualified as Foundation
-import Test.Unit.Identity qualified as Identity
-import Test.Unit.Html qualified as Html
-import Test.Unit.HtmlLayout qualified as HtmlLayout
-import Test.Unit.HtmlOutput qualified as HtmlOutput
-import Test.Unit.Kernel qualified as Kernel
-import Test.Unit.Lexicon qualified as Lexicon
-import Test.Unit.Meaning qualified as Meaning
-import Test.Unit.Materialization qualified as Materialization
-import Test.Unit.Module qualified as Module
-import Test.Unit.OutputPlan qualified as OutputPlan
-import Test.Unit.Provers qualified as Provers
-import Test.Unit.Semantic qualified as Semantic
-import Test.Unit.Source qualified as Source
-import Test.Unit.Store qualified as Store
-import Test.Unit.Token qualified as Token
-
-unitTests :: TestTree
-unitTests = testGroup "unit tests"
-    [ Abstract.unitTests
-    , Backend.unitTests
-    , CommandLine.unitTests
-    , Concrete.unitTests
-    , Core.unitTests
-    , Declaration.unitTests
-    , Foundation.unitTests
-    , Identity.unitTests
-    , Html.unitTests
-    , HtmlLayout.unitTests
-    , HtmlOutput.unitTests
-    , Kernel.unitTests
-    , Lexicon.unitTests
-    , Meaning.unitTests
-    , Materialization.unitTests
-    , Module.unitTests
-    , OutputPlan.unitTests
-    , Provers.unitTests
-    , Semantic.unitTests
-    , Source.unitTests
-    , Store.unitTests
-    , Token.unitTests
-    ]