diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -6,6 +6,12 @@
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [PVP versioning](https://pvp.haskell.org/).
 
+## v2.6.1 _(2024-09-02)_
+
+### Added
+- Added module 'Language.Hasmtlib.Type.Relation' for encoding binary relations
+- Added rich documentation and usage examples for all public modules
+
 ## v2.6.0 _(2024-08-27)_
 
 ### Added
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -2,7 +2,7 @@
 
 # Hasmtlib - Haskell SMTLib MTL Library
 
-Hasmtlib is a library for generating SMTLib2-problems using a monad.
+Hasmtlib is a library with high-level-abstraction for generating SMTLib2-problems using a monad.
 It takes care of encoding your problem, marshaling the data to an external solver and parsing and interpreting the result into Haskell types.
 It is highly inspired by [ekmett/ersatz](https://github.com/ekmett/ersatz) which does the same for QSAT. Communication with external solvers is handled by [tweag/smtlib-backends](https://github.com/tweag/smtlib-backends).
 
@@ -57,7 +57,7 @@
 
 ## Features
 
-- [x] SMTLib2-Sorts in the Haskell-Type
+- [x] SMTLib2-Sorts in the Haskell-Type to guarantee well-typed expressions
   ```haskell
     data SMTSort =
         BoolSort
@@ -72,43 +72,10 @@
   ```
 - [x] Full SMTLib 2.6 standard support for Sorts Bool, Int, Real, BitVec, Array & String
 - [x] Type-level length-indexed Bitvectors with type-level encoding (Signed/Unsigned) for BitVec
-  ```haskell
-  bvConcat :: (KnownNat n, KnownNat m) => Expr (BvSort enc n) -> Expr (BvSort enc m) -> Expr (BvSort enc (n + m))
-  bvLShR :: KnownNat n => Expr (BvSort Unsigned n) -> Expr (BvSort enc n) -> Expr (BvSort Unsigned n)
-  bvAShR :: KnownNat n => Expr (BvSort Signed n) -> Expr (BvSort enc n) -> Expr (BvSort Signed n)
-  ```
 - [x] Pure API with plenty common instances: `Num`, `Floating`, `Bounded`, `Bits`, `Ixed` and many more
-  ```haskell
-    solveWith @SMT (solver yices) $ do
-      setLogic "QF_BV"
-      x <- var @(BvSort Signed 16)
-      let f = x >? 42 && (x `div` 84 === maxBound - 100)
-      assert f
-      return x
-  ```
 - [x] Add your own solvers via the [Solver type](https://github.com/bruderj15/Hasmtlib/blob/master/src/Language/Hasmtlib/Type/Solution.hs)
-  ```haskell
-    -- | Function that turns a state (usually SMT or OMT) into a result and a solution
-    type Solver s m = s -> m (Result, Solution)
-  ```
 - [x] Solvers via external processes: CVC5, Z3, Yices2-SMT, MathSAT, OptiMathSAT, OpenSMT & Bitwuzla
-- [x] Incremental solving
-  ```haskell
-      cvc5Living <- interactiveSolver cvc5
-      interactiveWith @Pipe cvc5Living $ do
-        setLogic "QF_LIA"
-        setOption $ Incremental True
-        setOption $ ProduceModels True
-        x <- var @IntSort
-        assert $ x === 42
-        result <- checkSat
-        push
-        assert $ x <? 0
-        (result, solution) <- solve
-        case result of
-          Sat   -> return solution
-          Unsat -> pop >> ...
-  ```
+- [x] Support for incremental solving
 - [x] Pure quantifiers `for_all` and `exists`
   ```haskell
     solveWith @SMT (solver z3) $ do
@@ -133,6 +100,30 @@
 
       return x
   ```
+
+## Related work
+- [ekmett/ersatz](https://hackage.haskell.org/package/ersatz):
+Huge inspiration for this library (some code stolen).
+We do for `SMT` what they do for `SAT`.
+- [hgoes/smtlib2](https://hackage.haskell.org/package/smtlib2):
+Their eDSL is highly expressive and focuses on well-typed SMT-expressions.
+But their approach is a little verbose and makes usage feel quite heavy.
+Their eDSL is also entirely monadic and therefore formula construction is painful.
+- [yav/simple-smt](https://hackage.haskell.org/package/simple-smt):
+They are lightweight but their types are weak and their API is barely embedded into Haskell.
+- [LevantErkok/sbv](https://hackage.haskell.org/package/sbv):
+While they "express properties about Haskell programs and automatically prove them using SMT",
+we instead use Haskell to simplify the encoding of SMT-Problems.
+They can do a whole lot (C-Code-Gen, Crypto-Stuff,...), which is cool, but adds weight.
+
+If you want highly specific implementations for different solvers, all their individual configurations and swallow the awkward typing,
+then use [hgoes/smtlib2](https://hackage.haskell.org/package/smtlib2).
+
+If you want to express properties about Haskell programs and automatically prove them using SMT,
+then use [LevantErkok/sbv](https://hackage.haskell.org/package/sbv).
+
+If you want to encode SMT-problems as lightweight and close to Haskell as possible, then use this library.
+I personally use it for scheduling/resource-allocation-problems.
 
 ## Examples
 There are some examples in [here](https://github.com/bruderj15/Hasmtlib/tree/master/src/Language/Hasmtlib/Example).
diff --git a/hasmtlib.cabal b/hasmtlib.cabal
--- a/hasmtlib.cabal
+++ b/hasmtlib.cabal
@@ -1,7 +1,7 @@
 cabal-version:         3.0
 
 name:                  hasmtlib
-version:               2.6.0
+version:               2.6.1
 synopsis:              A monad for interfacing with external SMT solvers
 description:           Hasmtlib is a library for generating SMTLib2-problems using a monad.
   It takes care of encoding your problem, marshaling the data to an external solver and parsing and interpreting the result into Haskell types.
@@ -56,8 +56,10 @@
                      , Language.Hasmtlib.Type.Option
                      , Language.Hasmtlib.Type.ArrayMap
                      , Language.Hasmtlib.Type.Bitvec
+                     , Language.Hasmtlib.Type.Relation
 
-  build-depends:       attoparsec                   >= 0.14.4 && < 1
+  build-depends:       array                        >= 0.5    && < 1
+                     , attoparsec                   >= 0.14.4 && < 1
                      , base                         >= 4.17.2 && < 5
                      , bytestring                   >= 0.11.5 && < 1
                      , containers                   >= 0.6.7  && < 1
diff --git a/src/Language/Hasmtlib.hs b/src/Language/Hasmtlib.hs
--- a/src/Language/Hasmtlib.hs
+++ b/src/Language/Hasmtlib.hs
@@ -1,28 +1,49 @@
 module Language.Hasmtlib
   (
-    module Language.Hasmtlib.Type.MonadSMT
+    -- * Type
+    -- ** Expr
+    module Language.Hasmtlib.Type.SMTSort
+  , module Language.Hasmtlib.Type.Value
+  , module Language.Hasmtlib.Type.Expr
+
+    -- ** Containers
+  , module Language.Hasmtlib.Type.Bitvec
+  , module Language.Hasmtlib.Type.ArrayMap
+  , module Language.Hasmtlib.Type.Relation
+
+    -- ** SMT
+  , module Language.Hasmtlib.Type.MonadSMT
   , module Language.Hasmtlib.Type.SMT
+  , module Language.Hasmtlib.Type.Option
+
+  -- ** OMT
   , module Language.Hasmtlib.Type.OMT
+
+  -- ** Pipe
   , module Language.Hasmtlib.Type.Pipe
-  , module Language.Hasmtlib.Type.Expr
-  , module Language.Hasmtlib.Type.Value
-  , module Language.Hasmtlib.Type.Solver
-  , module Language.Hasmtlib.Type.Option
-  , module Language.Hasmtlib.Type.SMTSort
-  , module Language.Hasmtlib.Type.Solution
-  , module Language.Hasmtlib.Type.ArrayMap
-  , module Language.Hasmtlib.Type.Bitvec
-  , module Language.Hasmtlib.Boolean
+
+  -- * Class
   , module Language.Hasmtlib.Codec
+  , module Language.Hasmtlib.Boolean
   , module Language.Hasmtlib.Counting
   , module Language.Hasmtlib.Variable
+
+  -- * Solver
+  -- ** Type
+  , module Language.Hasmtlib.Type.Solution
+  , module Language.Hasmtlib.Type.Solver
   , module Language.Hasmtlib.Solver.Common
-  , module Language.Hasmtlib.Solver.Bitwuzla
-  , module Language.Hasmtlib.Solver.CVC5
+
+  -- ** Concrete solvers
   , module Language.Hasmtlib.Solver.Z3
+  , module Language.Hasmtlib.Solver.CVC5
   , module Language.Hasmtlib.Solver.Yices
   , module Language.Hasmtlib.Solver.OpenSMT
   , module Language.Hasmtlib.Solver.MathSAT
+  , module Language.Hasmtlib.Solver.Bitwuzla
+
+  -- * Internal
+  -- ** Sharing
   , SharingMode(..), setSharingMode
   )
   where
@@ -39,6 +60,7 @@
 import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Type.ArrayMap
 import Language.Hasmtlib.Type.Bitvec
+import Language.Hasmtlib.Type.Relation
 import Language.Hasmtlib.Boolean
 import Language.Hasmtlib.Codec
 import Language.Hasmtlib.Counting
diff --git a/src/Language/Hasmtlib/Boolean.hs b/src/Language/Hasmtlib/Boolean.hs
--- a/src/Language/Hasmtlib/Boolean.hs
+++ b/src/Language/Hasmtlib/Boolean.hs
@@ -1,13 +1,45 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
-module Language.Hasmtlib.Boolean where
+{- |
+This module provides a more generic version of bool-like algebras than what the Prelude does for 'Bool'.
 
+The class 'Boolean' therefore overloads most of the Preludes operators like '(&&)'.
+
+However, as 'Bool' also features an instance of 'Boolean', you can simply hide the Prelude ones - not having to import either qualified.
+
+==== __Example__
+
+@
+import Prelude hiding (not, any, all, (&&), (||), and, or)
+import Language.Hasmtlib
+
+problem :: MonadSMT s m => StateT s m (Expr BoolSort, Expr BoolSort)
+problem = do
+  x <- var \@BoolSort
+  y <- var
+  let b = False || True
+  assert $ x && y \<==\> and [x, y, true] && encode b ==> x && y
+  return (x,y)
+@
+-}
+module Language.Hasmtlib.Boolean
+(
+  -- * Class
+  Boolean(..)
+
+  -- * Operators
+, and, or
+, nand, nor
+, all, any
+)
+where
+
 import Prelude (Bool(..), (.), id, Eq(..))
 import qualified Prelude as P
 import Data.Bit
 import Data.Coerce
 import Data.Bits as Bits
-import Data.Foldable hiding (and, or)
+import Data.Foldable hiding (and, or, all, any)
 import qualified Data.Vector.Unboxed.Sized as V
 import GHC.TypeNats
 
diff --git a/src/Language/Hasmtlib/Codec.hs b/src/Language/Hasmtlib/Codec.hs
--- a/src/Language/Hasmtlib/Codec.hs
+++ b/src/Language/Hasmtlib/Codec.hs
@@ -3,8 +3,32 @@
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE ViewPatterns #-}
 
-module Language.Hasmtlib.Codec where
+{- |
+This module provides the class 'Codec' which takes care of marshalling data to and from external SMT-Solvers.
 
+A generic default implementation with 'GCodec' is possible.
+
+==== __Example__
+
+@
+data V3 a = V3 a a a deriving Generic
+instance Codec a => Codec (V3 a)
+
+constantV3 :: V3 (Expr RealSort)
+constantV3 = encode $ V3 7 69 42
+@
+-}
+module Language.Hasmtlib.Codec
+(
+  -- * Class
+  Codec(..)
+
+  -- * Generics
+, GCodec(..)
+, DefaultDecoded
+)
+where
+
 import Prelude hiding (not, (&&), (||), all, and)
 import Language.Hasmtlib.Type.Bitvec
 import Language.Hasmtlib.Type.Expr (Expr(..), SMTVar(..))
@@ -23,6 +47,7 @@
 import Data.IntMap as IM hiding (foldl)
 import Data.Dependent.Map as DMap
 import Data.Tree (Tree)
+import Data.Array (Array, Ix)
 import qualified Data.Text as Text
 import Data.Monoid (Sum, Product, First, Last, Dual)
 import qualified Data.Vector.Sized as V
@@ -31,7 +56,7 @@
 import GHC.Generics
 import GHC.TypeLits
 
--- | Computes a default 'Decoded' 'Type' by distributing 'Decoded' to it's type arguments.
+-- | Computes a default 'Decoded' 'Type' by distributing 'Decoded' over it's type arguments.
 type family DefaultDecoded a :: Type where
   DefaultDecoded (t a b c d e f g h) = t (Decoded a) (Decoded b) (Decoded c) (Decoded d) (Decoded e) (Decoded f) (Decoded g) (Decoded h)
   DefaultDecoded (t a b c d e f g) = t (Decoded a) (Decoded b) (Decoded c) (Decoded d) (Decoded e) (Decoded f) (Decoded g)
@@ -182,16 +207,21 @@
 instance Codec a => Codec (Identity a)
 
 instance Codec a => Codec (IntMap a) where
-  decode sol = traverse (decode sol)
+  decode = traverse . decode
   encode = fmap encode
 
 instance Codec a => Codec (Seq a) where
-  decode sol = traverse (decode sol)
+  decode = traverse . decode
   encode = fmap encode
 
 instance Codec a => Codec (Map k a) where
   type Decoded (Map k a) = Map k (Decoded a)
-  decode sol = traverse (decode sol)
+  decode = traverse . decode
+  encode = fmap encode
+
+instance (Ix i, Codec e) => Codec (Array i e) where
+  type Decoded (Array i e) = Array i (Decoded e)
+  decode = traverse . decode
   encode = fmap encode
 
 class GCodec f where
diff --git a/src/Language/Hasmtlib/Counting.hs b/src/Language/Hasmtlib/Counting.hs
--- a/src/Language/Hasmtlib/Counting.hs
+++ b/src/Language/Hasmtlib/Counting.hs
@@ -1,4 +1,32 @@
-module Language.Hasmtlib.Counting where
+{- |
+This module provides functions for counting symbolic formulas and creating cardinality-constraints.
+
+Internally this converts each given 'Expr' 'BoolSort' into a numerical 'Expr' using 'ite', then sums them up:
+
+@
+  count :: forall t f. (Functor f, Foldable f, Num (Expr t)) => f (Expr BoolSort) -> Expr t
+  count = sum . fmap (\\b -> ite b 1 0)
+@
+
+Therefore additional information for the temporal summation may need to be provided.
+
+E.g. if your logic is \"QF_LIA\" you would want @count \@IntSort $ ...@
+-}
+module Language.Hasmtlib.Counting
+(
+  -- * Count
+  count, count'
+
+  -- * At-Least
+, atLeast
+
+  -- * Exactly
+, exactly
+
+  -- * At-Most
+, atMost
+)
+where
 
 import Prelude hiding (not, (&&), (||), or)
 import Language.Hasmtlib.Type.SMTSort
diff --git a/src/Language/Hasmtlib/Internal/Parser.hs b/src/Language/Hasmtlib/Internal/Parser.hs
--- a/src/Language/Hasmtlib/Internal/Parser.hs
+++ b/src/Language/Hasmtlib/Internal/Parser.hs
@@ -7,6 +7,7 @@
 import Language.Hasmtlib.Internal.Render
 import Language.Hasmtlib.Boolean
 import Language.Hasmtlib.Codec
+import Language.Hasmtlib.Type.Value
 import Language.Hasmtlib.Type.Bitvec
 import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Solution
diff --git a/src/Language/Hasmtlib/Solver/Bitwuzla.hs b/src/Language/Hasmtlib/Solver/Bitwuzla.hs
--- a/src/Language/Hasmtlib/Solver/Bitwuzla.hs
+++ b/src/Language/Hasmtlib/Solver/Bitwuzla.hs
@@ -9,11 +9,3 @@
 --   Make sure it's default SAT-Solver binary - probably @cadical@ - is in path too.
 bitwuzla :: Config
 bitwuzla = defaultConfig { exe = "bitwuzla", args = [] }
-
--- | A 'Config' for Bitwuzla which uses Kissat for SAT-Solving.
---   Requires binary @bitwuzla@ and @kissat@ to be in path.
---
--- Combination with Kissat currently behaves weirdly: https://github.com/bitwuzla/bitwuzla/issues/119
---
--- bitwuzlaWithKissat :: Config
--- bitwuzlaWithKissat = defaultConfig { exe = "bitwuzla", args = ["--sat-solver=kissat"] }
diff --git a/src/Language/Hasmtlib/Solver/Common.hs b/src/Language/Hasmtlib/Solver/Common.hs
--- a/src/Language/Hasmtlib/Solver/Common.hs
+++ b/src/Language/Hasmtlib/Solver/Common.hs
@@ -1,5 +1,25 @@
-module Language.Hasmtlib.Solver.Common where
+{- |
+This module handles common IO interaction with external SMT-Solvers via external processes.
 
+It is built on top of Tweag's package @smtlib-backends@.
+
+Although there already are several concrete solvers like @Z3@ in @Language.Hasmtlib.Solver.Z3@,
+you may use this module to create your own solver bindings.
+-}
+module Language.Hasmtlib.Solver.Common
+(
+  -- * Construction
+  processSolver
+, solver
+, interactiveSolver
+
+  -- * Debugging
+, Debugger(..)
+, debug
+, def
+)
+where
+
 import Language.Hasmtlib.Type.SMT
 import Language.Hasmtlib.Type.OMT
 import Language.Hasmtlib.Type.Solution
@@ -67,14 +87,15 @@
 --
 -- 1. Encode the 'SMT'-problem,
 --
--- 2. Start a new external process for the SMT-Solver,
+-- 2. start a new external process for the SMT-Solver,
 --
--- 3. Send the problem to the SMT-Solver,
+-- 3. send the problem to the SMT-Solver,
 --
--- 4. Wait for an answer and parse it and
+-- 4. wait for an answer and parse it,
 --
--- 5. close the process and clean up all resources.
+-- 5. close the process and clean up all resources and
 --
+-- 6. return the decoded solution.
 processSolver :: (RenderSeq s, MonadIO m) => Process.Config -> Maybe (Debugger s) -> Solver s m
 processSolver cfg debugger s = do
   liftIO $ Process.with cfg $ \handle -> do
diff --git a/src/Language/Hasmtlib/Type/ArrayMap.hs b/src/Language/Hasmtlib/Type/ArrayMap.hs
--- a/src/Language/Hasmtlib/Type/ArrayMap.hs
+++ b/src/Language/Hasmtlib/Type/ArrayMap.hs
@@ -1,8 +1,24 @@
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE UndecidableInstances #-}
 
-module Language.Hasmtlib.Type.ArrayMap where
+{- |
+This module provides a class 'ArrayMap' and a concrete implementation with 'ConstArray' for
+McCarthy's basic array theory.
+-}
+module Language.Hasmtlib.Type.ArrayMap
+(
+  -- * Class
+  ArrayMap(..)
+, asConst
 
+  -- * Type
+, ConstArray(..)
+
+  -- * Lens
+, arrConst, stored
+)
+where
+
 import Data.Proxy
 import qualified Data.Map as Map
 import Control.Lens
@@ -15,16 +31,25 @@
 --
 --   Therefore the following axioms must hold:
 --
--- 1. forall A i x: arrSelect (store A i x) == x
+-- 1. forall A i x: arrSelect (arrStore i x) == x
 --
--- 2. forall A i j x: i /= j ==> (arrSelect (arrStore A i x) j === arrSelect A j)
+-- 2. forall A i j x: i /= j ==> (arrSelect (arrStore i x) j === arrSelect A j)
 class ArrayMap f k v where
+  -- | Construct an 'ArrayMap' via it's const value.
   asConst'   :: Proxy f -> Proxy k -> v -> f k v
+
+  -- | View the const value of the 'ArrayMap'.
   viewConst  :: f k v -> v
-  arrSelect  :: f k v -> k -> v
-  arrStore   :: f k v -> k -> v -> f k v
 
--- | Wrapper for 'asConst'' which hides the 'Proxy'
+  -- | Select a value from the 'ArrayMap'.
+  --
+  -- Returns the specific value for given key if there is one. Returns the const value otherwise.
+  arrSelect :: f k v -> k -> v
+
+  -- | Store a specific value at a given key in an 'ArrayMap'.
+  arrStore :: f k v -> k -> v -> f k v
+
+-- | Wrapper for 'asConst'' which hides the 'Proxy'.
 asConst :: forall f k v. ArrayMap f k v => v -> f k v
 asConst = asConst' (Proxy @f) (Proxy @k)
 
diff --git a/src/Language/Hasmtlib/Type/Bitvec.hs b/src/Language/Hasmtlib/Type/Bitvec.hs
--- a/src/Language/Hasmtlib/Type/Bitvec.hs
+++ b/src/Language/Hasmtlib/Type/Bitvec.hs
@@ -2,12 +2,44 @@
 {-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE RoleAnnotations #-}
 
+{- |
+This module provides the type-level length-indexed and MSB-first bitvector 'Bitvec'
+built on top of the package @bitvec@ and 'V.Vector'.
+
+It also holds it's type of encoding as a phantom-type via 'BvEnc'.
+
+==== __Examples__
+
+>>> minBound @(Bitvec Unsigned 8)
+00000000
+
+>>> maxBound @(Bitvec Signed 8)
+01111111
+
+>>> (5 :: Bitvec Unsigned 4) + 10
+1111
+-}
 module Language.Hasmtlib.Type.Bitvec
-( BvEnc(..), SBvEnc(..), KnownBvEnc(..)
+(
+  -- * Bitvector encoding
+  BvEnc(..), SBvEnc(..), KnownBvEnc(..)
 , bvEncSing', bvEncSing''
+
+  -- * Bitvec type
 , Bitvec(..)
+
+  -- * Construction
+, bitvecConcat
+
+  -- * Conversion
+  -- ** Sign
 , asUnsigned, asSigned
-, bitvecConcat, bitvecFromListN, bitvecFromListN'
+
+  -- ** Lists
+, bitvecFromListN, bitvecFromListN'
+
+  -- * Lens
+, _signBit
 )
 where
 
@@ -24,6 +56,7 @@
 import Data.Bifunctor
 import Data.Type.Equality
 import qualified Data.Vector.Unboxed.Sized as V
+import Control.Lens
 import GHC.TypeNats
 
 -- | Type of Bitvector encoding - used as promoted type (data-kind).
@@ -66,6 +99,7 @@
   -- gcompare _ SSigned  = GGT
 
 -- | Length-indexed bitvector ('V.Vector') carrying a phantom type-level 'BvEnc'.
+--
 --   Most significant bit is first (index 0) for unsigned bitvectors.
 --   Signed bitvectors have their sign bit first (index 0) and their most significant bit second (index 1).
 type role Bitvec phantom phantom
@@ -140,11 +174,21 @@
   toInteger = fromIntegral . fromEnum
   quotRem x y = bimap fromInteger fromInteger $ quotRem (toInteger x) (toInteger y)
 
+-- | A Lens on the sign-bit of a signed bitvector.
+_signBit :: KnownNat (n + 1) => Lens' (Bitvec Signed (n + 1)) Bit
+_signBit = lens (\bv -> Bit $ testBit bv 0 )$
+  \bv b -> case b of
+    Bit False -> clearBit bv 0
+    Bit True  -> setBit   bv 0
+
+-- | Concatenation of two bitvectors.
 bitvecConcat :: Bitvec enc n -> Bitvec enc m -> Bitvec enc (n + m)
 bitvecConcat (coerce -> x) (coerce -> y) = coerce $ x V.++ y
 
+-- | Constructing a bitvector from a list.
 bitvecFromListN :: forall n enc. KnownNat n => [Bit] -> Maybe (Bitvec enc n)
 bitvecFromListN = coerce . V.fromListN @n
 
+-- | Constructing a bitvector from a list with length given as 'Proxy'.
 bitvecFromListN' :: KnownNat n => Proxy n -> [Bit] -> Maybe (Bitvec enc n)
 bitvecFromListN' _ = bitvecFromListN
diff --git a/src/Language/Hasmtlib/Type/Expr.hs b/src/Language/Hasmtlib/Type/Expr.hs
--- a/src/Language/Hasmtlib/Type/Expr.hs
+++ b/src/Language/Hasmtlib/Type/Expr.hs
@@ -5,17 +5,73 @@
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE DerivingStrategies #-}
 
+{- |
+This module provides the data-type 'Expr'.
+
+It represents SMTLib-expressions via an abstract syntax tree (AST), implemented as GADT.
+
+Variables are just 'Int's wrapped in a newtype 'SMTVar' with a phantom-type 'SMTSort'.
+
+Usually the end user of this library does not need to deal with this representation.
+Instead he should rely on the provided instances for building expressions.
+Some of the main classes of these include:
+
+1. 'Equatable' and 'Orderable' for symbolic comparisons,
+
+2. 'Iteable' for symbolic branching via 'ite',
+
+3. 'Boolean' for symbolic bool operations,
+
+4. Prelude classics like: 'Num', 'Floating', 'Integral', 'Bounded', ... for arithmetics
+
+5. 'Bits.Bits' for BitVec-operations
+
+Besides that, there are also some operations defined by the SMTLib-Standard Version 2.6 that do not fit into any classes
+and therefore are exported as plain functions, like 'for_all' or 'bvConcat'.
+-}
 module Language.Hasmtlib.Type.Expr
-  ( SMTVar(..), varId
-  , Value(..) , unwrapValue, wrapValue
+  (
+  -- * SMTVar
+    SMTVar(..), varId
+
+  -- * Expr type
   , Expr(..), isLeaf
-  , Iteable(..), Equatable(..), Orderable(..), min', max'
+
+  -- * Compare
+  -- ** Equatable
+  -- *** Class
+  , Equatable(..)
   , equal, distinct
+
+  -- *** Generic
+  , GEquatable(..)
+
+  -- ** Orderable
+  -- *** Class
+  , Orderable(..)
+  , min', max'
+
+  -- *** Generic
+  , GOrderable(..)
+
+  -- ** Iteable
+  , Iteable(..)
+
+  -- * Non-class functions
+  -- ** Quantifier
   , for_all, exists
+
+  -- ** BitVec
+  , bvConcat
+
+  -- ** Array
   , select, store
-  , bvShL, bvLShR, bvAShR, bvConcat
-  , toRealSort, toIntSort, isIntSort
+
+  -- ** String
   , strLength, strAt, strSubstring, strPrefixOf, strSuffixOf, strContains, strIndexOf, strReplace, strReplaceAll
+
+  -- ** Conversion
+  , toRealSort, toIntSort, isIntSort
   )
 where
 
@@ -59,9 +115,9 @@
 $(makeLenses ''SMTVar)
 
 -- | An SMT-Expression.
---   For building expressions use the corresponding instances: 'Boolean', 'Num', 'Equatable', ...
+--   For building expressions use the corresponding instances.
 --
---   With a lot of criminal energy you may build invalid expressions regarding the SMTLib Version 2.6 - Specification.
+--   With a lot of criminal energy you may build invalid expressions regarding the SMTLib Version 2.6 - specification.
 --   Therefore it is highly recommended to rely on the instances.
 data Expr (t :: SMTSort) where
   Var       :: KnownSMTSort t => SMTVar t -> Expr t
@@ -125,7 +181,7 @@
   Exists    :: KnownSMTSort t => Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Expr BoolSort
 
 -- | Indicates whether an expression is a leaf.
---   All non-recursive contructors form leafs.
+--   All non-recursive contructors are leafs.
 isLeaf :: Expr t -> Bool
 isLeaf (Var _) = True
 isLeaf (Constant _) = True
@@ -133,11 +189,17 @@
 isLeaf _ = False
 {-# INLINE isLeaf #-}
 
--- | If condition (p :: b) then (t :: a) else (f :: a)
+-- | Class that allows branching on predicates of type @b@ on branches of type @a@.
 --
---    >>> ite true "1" "2"
+--   If predicate (p :: b) then (t :: a) else (f :: a).
+--
+--   There is a default implementation if your type is an 'Applicative'.
+--
+-- ==== __Examples__
+--
+--    >>> ite True "1" "2"
 --        "1"
---    >>> ite false 100 42
+--    >>> ite False 100 42
 --        42
 class Iteable b a where
   ite :: b -> a -> a -> a
@@ -187,16 +249,17 @@
 instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d, Iteable (Expr BoolSort) e, Iteable (Expr BoolSort) f, Iteable (Expr BoolSort) g, Iteable (Expr BoolSort) h) => Iteable (Expr BoolSort) (a,b,c,d,e,f,g,h) where
   ite p (a,b,c,d,e,f,g,h) (a',b',c',d',e',f',g',h') = (ite p a a', ite p b b', ite p c c', ite p d d', ite p e e', ite p f f', ite p g g', ite p h h')
 
--- | Test two as on equality as SMT-Expression.
+-- | Symbolically test two values on equality.
 --
---   You can derive an instance of this class if your type is 'Generic'.
+-- A generic default implementation with 'GEquatable' is possible.
 --
+-- ==== __Example__
+--
 -- @
---     x <- var @RealType
---     y <- var
---     assert $ y === x && not (y /== x)
+-- x <- var @RealType
+-- y <- var
+-- assert $ y === x && not (y /== x) && x === 42
 -- @
---
 class Equatable a where
   -- | Test whether two values are equal in the SMT-Problem.
   (===) :: a -> a -> Expr BoolSort
@@ -275,10 +338,12 @@
 instance Equatable a => Equatable (Dual a)
 instance Equatable a => Equatable (Identity a)
 
--- | Compare two as as SMT-Expression.
+-- | Symbolically compare two values.
 --
---   You can derive an instance of this class if your type is 'Generic'.
+-- A generic default implementation with 'GOrderable' is possible.
 --
+-- ==== __Example__
+--
 -- @
 -- x <- var @RealSort
 -- y <- var
@@ -302,11 +367,11 @@
 
 infix 4 <?, <=?, >=?, >?
 
--- | Minimum of two as SMT-Expression.
+-- | Symbolic evaluation of the minimum of two symbolic values.
 min' :: (Orderable a, Iteable (Expr BoolSort) a) => a -> a -> a
 min' x y = ite (x <=? y) x y
 
--- | Maximum of two as SMT-Expression.
+-- | Symbolic evaluation of the maximum of two symbolic values.
 max' :: (Orderable a, Iteable (Expr BoolSort) a) => a -> a -> a
 max' x y = ite (y <=? x) x y
 
@@ -356,7 +421,6 @@
   K1 a <=?# K1 b = a <=? b
 
 -- Boring instances that end up being useful when deriving Orderable with Generics
-
 instance Orderable ()       where _ <?  _ = false
                                   _ <=? _ = true
 instance Orderable Void     where x <?  y = x `seq` y `seq` error "Orderable[Void].<?"
@@ -414,7 +478,9 @@
 instance Orderable a => Orderable (Dual a)
 instance Orderable a => Orderable (Identity a)
 
--- | Test multiple expressions on equality within in the 'SMT'-Problem.
+-- | Symbolically test multiple expressions on equality.
+--
+--   Returns 'true' if given less than two arguments.
 equal :: (Eq (HaskellType t), KnownSMTSort t, Foldable f) => f (Expr t) -> Expr BoolSort
 equal (toList -> (a:b:xs)) = case someNatVal (genericLength xs) of
   SomeNat n -> case V.fromListN' n xs of
@@ -422,7 +488,9 @@
     Just xs' -> EQU $ xs' V.++ V.fromTuple (a,b)
 equal (toList -> _)        = true
 
--- | Test multiple expressions on distinctness within in the 'SMT'-Problem.
+-- | Symbolically test multiple expressions on distinctness.
+--
+--   Returns 'true' if given less than two arguments.
 distinct :: (Eq (HaskellType t), KnownSMTSort t, Foldable f) => f (Expr t) -> Expr BoolSort
 distinct (toList -> (a:b:xs)) = case someNatVal (genericLength xs) of
   SomeNat n -> case V.fromListN' n xs of
@@ -430,11 +498,9 @@
     Just xs' -> Distinct $ xs' V.++ V.fromTuple (a,b)
 distinct (toList -> _)        = true
 
--- | A universal quantification for any specific 'SMTSort'.
---   If the type cannot be inferred, apply a type-annotation.
---   Nested quantifiers are also supported.
+-- | Universal quantification for any specific 'SMTSort'.
 --
---   Usage:
+-- ==== __Example__
 --
 --   @
 --   assert $
@@ -448,15 +514,13 @@
 for_all = ForAll Nothing
 {-# INLINE for_all #-}
 
--- | An existential quantification for any specific 'SMTSort'
---   If the type cannot be inferred, apply a type-annotation.
---   Nested quantifiers are also supported.
+-- | Existential quantification for any specific 'SMTSort'
 --
---   Usage:
+-- ==== __Example__
 --
 --   @
 --   assert $
---      for_all @(BvSort 8) $ \x ->
+--      for_all @(BvSort Unsigned 8) $ \x ->
 --          exists $ \y ->
 --            x - y === 0
 --   @
@@ -477,21 +541,6 @@
 store = ArrStore
 {-# INLINE store #-}
 
--- | Logically shift left the first expression by the second expression.
-bvShL    :: (KnownBvEnc enc, KnownNat n) => Expr (BvSort enc n) -> Expr (BvSort enc n) -> Expr (BvSort enc n)
-bvShL    = BvShL
-{-# INLINE bvShL #-}
-
--- | Logically shift right the first expression by the second expression.
-bvLShR   :: KnownNat n => Expr (BvSort Unsigned n) -> Expr (BvSort Unsigned n) -> Expr (BvSort Unsigned n)
-bvLShR   = BvLShR
-{-# INLINE bvLShR #-}
-
--- | Arithmetically shift right the first expression by the second expression.
-bvAShR   :: KnownNat n => Expr (BvSort Signed n) -> Expr (BvSort Signed n) -> Expr (BvSort Signed n)
-bvAShR   = BvAShR
-{-# INLINE bvAShR #-}
-
 -- | Concats two bitvectors.
 bvConcat :: (KnownBvEnc enc, KnownNat n, KnownNat m) => Expr (BvSort enc n) -> Expr (BvSort enc m) -> Expr (BvSort enc (n + m))
 bvConcat = BvConcat
@@ -533,25 +582,25 @@
 {-# INLINE strSubstring #-}
 
 -- | First string is a prefix of second one.
---   @(str.prefixof s t)@ is @true@ iff @s@ is a prefix of @t@.
+--   @(strPrefixof s t)@ is @true@ iff @s@ is a prefix of @t@.
 strPrefixOf :: Expr StringSort -> Expr StringSort -> Expr BoolSort
 strPrefixOf = StrPrefixOf
 {-# INLINE strPrefixOf #-}
 
 -- | First string is a suffix of second one.
---   @(str.suffixof s t)@ is @true@ iff @s@ is a suffix of @t@.
+--   @(strSuffixof s t)@ is @true@ iff @s@ is a suffix of @t@.
 strSuffixOf :: Expr StringSort -> Expr StringSort -> Expr BoolSort
 strSuffixOf = StrSuffixOf
 {-# INLINE strSuffixOf #-}
 
 -- | First string contains second one
---   @(str.contains s t)@ iff @s@ contains @t@.
+--   @(strContains s t)@ iff @s@ contains @t@.
 strContains :: Expr StringSort -> Expr StringSort -> Expr BoolSort
 strContains = StrContains
 {-# INLINE strContains #-}
 
 -- | Index of first occurrence of second string in first one starting at the position specified by the third argument.
---   @(str.indexof s t i)@, with @0 <= i <= |s|@ is the position of the first
+--   @(strIndexof s t i)@, with @0 <= i <= |s|@ is the position of the first
 --   occurrence of @t@ in @s@ at or after position @i@, if any.
 --   Otherwise, it is @-1@. Note that the result is @i@ whenever @i@ is within
 --   the range @[0, |s|]@ and @t@ is empty.
@@ -559,7 +608,7 @@
 strIndexOf = StrIndexOf
 {-# INLINE strIndexOf #-}
 
--- | @(str.replace s t t')@ is the string obtained by replacing the first
+-- | @(strReplace s t t')@ is the string obtained by replacing the first
 --   occurrence of @t@ in @s@, if any, by @t'@. Note that if @t@ is empty, the
 --   result is to prepend @t'@ to @s@; also, if @t@ does not occur in @s@ then
 --   the result is @s@.
@@ -567,7 +616,7 @@
 strReplace = StrReplace
 {-# INLINE strReplace #-}
 
--- | @(str.replace_all s t t’)@ is @s@ if @t@ is the empty string. Otherwise, it
+-- | @(strReplaceAll s t t’)@ is @s@ if @t@ is the empty string. Otherwise, it
 --   is the string obtained from @s@ by replacing all occurrences of @t@ in @s@
 --   by @t’@, starting with the first occurrence and proceeding in left-to-right order.
 strReplaceAll :: Expr StringSort -> Expr StringSort -> Expr StringSort -> Expr StringSort
diff --git a/src/Language/Hasmtlib/Type/MonadSMT.hs b/src/Language/Hasmtlib/Type/MonadSMT.hs
--- a/src/Language/Hasmtlib/Type/MonadSMT.hs
+++ b/src/Language/Hasmtlib/Type/MonadSMT.hs
@@ -1,8 +1,35 @@
 {-# LANGUAGE LambdaCase #-}
 
-module Language.Hasmtlib.Type.MonadSMT where
+{- |
+This module provides MTL-Style-classes for building SMT-problems.
 
+The following three classes form the core of this module:
+
+1. 'MonadSMT' for plain SMT-problems. Create variables using 'var' and assert formulas via 'assert'.
+
+2. 'MonadIncrSMT' for plain SMT-problems with addtional access to the external solvers incremental stack and it's operations.
+
+3. 'MonadOMT' for SMT-problems with optimization. Optimize via 'minimize' and 'maximize' and softly assert formulas via 'assertSoft'.
+-}
+module Language.Hasmtlib.Type.MonadSMT
+(
+  -- * MonadSMT
+  MonadSMT(..)
+, var, smtvar
+, constant, assertMaybe, quantify
+
+  -- * MonadIncrSMT
+, MonadIncrSMT(..)
+, solve
+
+  -- * MonadOMT
+, MonadOMT(..)
+, assertSoftWeighted
+)
+where
+
 import Language.Hasmtlib.Type.Expr
+import Language.Hasmtlib.Type.Value
 import Language.Hasmtlib.Type.Option
 import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Solution
@@ -13,33 +40,46 @@
 import Control.Monad.State
 
 -- | A 'MonadState' that holds an SMT-Problem.
+--
+-- ==== __Example__
+--
+-- @
+-- problem :: MonadSMT s m => StateT s m (Expr IntSort)
+-- problem = do
+--   setLogic \"QF_LIA\"
+--   x <- var @IntSort
+--   assert $ x + 2 === x * 2
+--   return x
+-- @
 class MonadState s m => MonadSMT s m where
   -- | Construct a variable.
   --   This is mainly intended for internal use.
   --   In the API use 'var'' instead.
-  --
-  -- @
-  -- x :: SMTVar RealType <- smtvar' (Proxy @RealType)
-  -- @
   smtvar' :: forall t. KnownSMTSort t => Proxy t -> m (SMTVar t)
 
   -- | Construct a variable as expression.
   --
+  -- ==== __Example__
+  --
   -- @
-  -- x :: Expr RealType <- var' (Proxy @RealType)
+  -- x <- var' (Proxy @RealType)
   -- @
   var' :: forall t. KnownSMTSort t => Proxy t -> m (Expr t)
 
   -- | Assert a boolean expression.
   --
+  -- ==== __Example__
+  --
   -- @
-  -- x :: Expr IntType <- var @IntType
-  -- assert $ x + 5 === 42
+  -- x <- var @IntType
+  -- assert $ x - 27 === 42
   -- @
   assert :: Expr BoolSort -> m ()
 
   -- | Set an SMT-Solver-Option.
   --
+  -- ==== __Example__
+  --
   -- @
   -- setOption $ Incremental True
   -- @
@@ -47,12 +87,20 @@
 
   -- | Set the logic for the SMT-Solver to use.
   --
+  -- ==== __Example__
+  --
   -- @
   -- setLogic \"QF_LRA\"
   -- @
   setLogic :: String -> m ()
 
 -- | Wrapper for 'var'' which hides the 'Proxy'.
+--
+-- ==== __Example__
+--
+-- @
+-- x <- var @BoolSort
+-- @
 var :: forall t s m. (KnownSMTSort t, MonadSMT s m) => m (Expr t)
 var = var' (Proxy @t)
 {-# INLINE var #-}
@@ -66,33 +114,36 @@
 
 -- | Create a constant.
 --
+-- ==== __Examples__
+--
 --   >>> constant True
 --       Constant (BoolValue True)
 --
---   >>> let x :: Integer = 10 ; constant x
+--   >>> constant (10 :: Integer)
 --       Constant (IntValue 10)
 --
---   >>> constant @IntType 5
---       Constant (IntValue 5)
+--   >>> constant @RealSort 5
+--       Constant (RealValue 5.0)
 --
---   >>> constant @(BvType 8) 5
---       Constant (BvValue 0000101)
+--   >>> constant @(BvSort Unsigned 8) 14
+--       Constant (BvValue 00001110)
 constant :: KnownSMTSort t => HaskellType t -> Expr t
 constant = Constant . wrapValue
 {-# INLINE constant #-}
 
 -- | Maybe assert a boolean expression.
+--
 --   Asserts given expression if 'Maybe' is a 'Just'.
 --   Does nothing otherwise.
 assertMaybe :: MonadSMT s m => Maybe (Expr BoolSort) -> m ()
 assertMaybe Nothing = return ()
 assertMaybe (Just expr) = assert expr
 
---   We need this separate so we get a pure API for quantifiers
---   Ideally we would do that when rendering the expression
---   However Language.Hasmtlib.Internal.Render#render is pure but we need a new quantified var which is stateful
 -- | Assign quantified variables to all quantified subexpressions of an expression.
---   This shall only be used internally.
+--
+--   Quantifies bottom-up.
+--
+--   This is intended for internal use.
 --   Usually before rendering an assert.
 quantify :: MonadSMT s m => KnownSMTSort t => Expr t -> m (Expr t)
 quantify = transformM (
@@ -107,7 +158,28 @@
         expr -> return expr
   )
 
--- | A 'MonadSMT' that allows incremental solving.
+-- | A 'MonadSMT' that addtionally allows incremental solving with access to a solvers incremental stack.
+--
+-- Some solvers require to have 'SMTOption' 'Incremental' set first.
+--
+-- ==== __Example__
+--
+-- @
+-- problem :: MonadIncrSMT s m => StateT s m ()
+-- problem = do
+--   setOption $ Incremental True
+--   setLogic \"QF_LIA\"
+--   x <- var @IntSort
+--   push
+--   assert $ x + 2 === x * 2
+--   res <- checkSat
+--   case res of
+--     Sat -> do
+--       x' <- getValue x
+--       ...
+--     _ -> pop ...
+--   return ()
+-- @
 class MonadSMT s m => MonadIncrSMT s m where
   -- | Push a new context (one) to the solvers context-stack.
   push :: m ()
@@ -115,28 +187,32 @@
   -- | Pop the solvers context-stack by one.
   pop :: m ()
 
-  -- | Run check-sat on the current problem.
+  -- | Run @check-sat@ on the current problem.
   checkSat :: m Result
 
   -- | Run get-model on the current problem.
   --   This can be used to decode temporary models within the SMT-Problem.
   --
+  -- ==== __Example__
+  --
   -- @
   -- x <- var @RealSort
   -- y <- var
   -- assert $ x >? y && y <? (-1)
   -- res <- checkSat
   -- case res of
-  --   Unsat -> print "Unsat. Cannot get model."
-  --   r     -> do
+  --   Sat -> do
   --     model <- getModel
   --     liftIO $ print $ decode model x
+  --   r -> print $ show r <> ": Cannot get model."
   -- @
   getModel :: m Solution
 
   -- | Evaluate any expressions value in the solvers model.
   --   Requires a 'Sat' or 'Unknown' check-sat response beforehand.
   --
+  -- ==== __Example__
+  --
   -- @
   -- x <- var @RealSort
   -- assert $ x >? 10
@@ -150,15 +226,39 @@
   getValue :: KnownSMTSort t => Expr t -> m (Maybe (Decoded (Expr t)))
 
 -- | First run 'checkSat' and then 'getModel' on the current problem.
+--
+-- ==== __Example__
+--
+-- @
+-- x <- var @BoolSort
+-- assert $ x `xor` false
+-- (res, sol) <- solve
+-- case res of
+--   Sat -> do
+--     x' <- getValue x
+--     liftIO $ print $ decode sol x
+--   r -> print r
+-- @
 solve :: (MonadIncrSMT s m, MonadIO m) => m (Result, Solution)
 solve = liftM2 (,) checkSat getModel
 
--- | A 'MonadState' that holds an OMT-Problem.
---   An OMT-Problem is a 'SMT-Problem' with additional optimization targets.
+-- | A 'MonadSMT' that addtionally allows optimization targets.
+--
+-- ==== __Example__
+--
+-- @
+-- problem :: MonadOMT s m => StateT s m (Expr (BvSort Unsigned 8))
+-- problem = do
+--   setLogic \"QF_BV\"
+--   x <- var @(BvSort Unsigned 8)
+--   assertSoftWeighted (x <? maxBound) 2.0
+--   maximize x
+--   return x
+-- @
 class MonadSMT s m => MonadOMT s m where
   -- | Minimizes a numerical expression within the OMT-Problem.
   --
-  --   For example, below minimization:
+  -- ==== __Example__
   --
   -- @
   -- x <- var @IntSort
@@ -166,38 +266,31 @@
   -- minimize x
   -- @
   --
-  --   will give @x := -1@ as solution.
+  -- will give @x := -1@ as solution.
   minimize :: (KnownSMTSort t, Num (Expr t)) => Expr t -> m ()
 
   -- | Maximizes a numerical expression within the OMT-Problem.
   --
-  --   For example, below maximization:
+  -- ==== __Example__
   --
   -- @
-  -- x <- var @(BvSort 8)
+  -- x <- var @(BvSort Signed 4)
+  -- assert $ x <? 2
   -- maximize x
   -- @
   --
-  --   will give @x := 11111111@ as solution.
+  -- will give @x := 0001@ as solution.
   maximize :: (KnownSMTSort t, Num (Expr t)) => Expr t -> m ()
 
-  -- | Asserts a soft boolean expression.
-  --   May take a weight and an identifier for grouping.
-  --
-  --   For example, below a soft constraint with weight 2.0 and identifier \"myId\" for grouping:
+  -- | Softly asserts a boolean expression.
   --
-  -- @
-  -- x <- var @BoolSort
-  -- assertSoft x (Just 2.0) (Just "myId")
-  -- @
+  --   May take a weight and an identifier for grouping.
   --
-  --   Omitting the weight will default it to 1.0.
+  -- ==== __Example__
   --
   -- @
   -- x <- var @BoolSort
-  -- y <- var @BoolSort
-  -- assertSoft x
-  -- assertSoft y (Just "myId")
+  -- assertSoft x (Just 0.5) (Just "myId")
   -- @
   assertSoft :: Expr BoolSort -> Maybe Double -> Maybe String -> m ()
 
diff --git a/src/Language/Hasmtlib/Type/OMT.hs b/src/Language/Hasmtlib/Type/OMT.hs
--- a/src/Language/Hasmtlib/Type/OMT.hs
+++ b/src/Language/Hasmtlib/Type/OMT.hs
@@ -2,7 +2,25 @@
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE LambdaCase #-}
 
-module Language.Hasmtlib.Type.OMT where
+{- |
+This module provides a concrete implementation for 'MonadOMT' with it's state 'OMT'.
+-}
+module Language.Hasmtlib.Type.OMT
+(
+  -- * SoftFormula
+  SoftFormula(..)
+
+  -- * Optimization targets
+, Minimize(..), Maximize(..)
+
+  -- * OMT
+  -- ** Type
+, OMT(..)
+
+  -- ** Lens
+, smt, targetMinimize, targetMaximize, softFormulas
+)
+where
 
 import Language.Hasmtlib.Internal.Sharing
 import Language.Hasmtlib.Internal.Render
diff --git a/src/Language/Hasmtlib/Type/Option.hs b/src/Language/Hasmtlib/Type/Option.hs
--- a/src/Language/Hasmtlib/Type/Option.hs
+++ b/src/Language/Hasmtlib/Type/Option.hs
@@ -1,3 +1,6 @@
+{- |
+This module provides the data-type 'SMTOption' for adjusting a SMT-Solvers options.
+-}
 module Language.Hasmtlib.Type.Option where
 
 import Language.Hasmtlib.Internal.Render
diff --git a/src/Language/Hasmtlib/Type/Pipe.hs b/src/Language/Hasmtlib/Type/Pipe.hs
--- a/src/Language/Hasmtlib/Type/Pipe.hs
+++ b/src/Language/Hasmtlib/Type/Pipe.hs
@@ -2,7 +2,22 @@
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE LambdaCase #-}
 
-module Language.Hasmtlib.Type.Pipe where
+{- |
+This module provides an IO-'Pipe' to external SMT-Solvers and ships with implementations for 'MonadSMT', 'MonadOMT' and 'MonadIncrSMT'.
+
+The 'Pipe' is based on a 'B.Solver' from Tweag's package @smtlib-backends@ and in reality is just an IO-Handle.
+-}
+module Language.Hasmtlib.Type.Pipe
+(
+  -- * Type
+  Pipe(..)
+
+  -- * Lens
+, lastPipeVarId, mPipeLogic
+, pipeSharingMode, pipeStableMap, incrSharedAuxs
+, pipeSolver, isDebugging
+)
+where
 
 import Language.Hasmtlib.Internal.Sharing
 import Language.Hasmtlib.Internal.Render
diff --git a/src/Language/Hasmtlib/Type/Relation.hs b/src/Language/Hasmtlib/Type/Relation.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Hasmtlib/Type/Relation.hs
@@ -0,0 +1,228 @@
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{- |
+This module provides the data-type 'Relation' for encoding binary relations as SMT-problems.
+
+==== __Example__
+
+@
+problem :: MonadSMT s m => StateT s m (Relation Int Int)
+    setLogic \"QF_LIA\"
+
+    r <- relation ((2,1), (6,5))
+
+    forM_ (image r \<$\> domain r) (assert . exactly \@IntSort 1)
+    forM_ (preimage r \<$\> codomain r) (assert . exactly \@IntSort 1)
+
+    assertMaybe $ do
+      item <- r^?ix (3,3)
+      return $ item === true
+
+    return r
+@
+-}
+module Language.Hasmtlib.Type.Relation
+(
+  -- * Type
+  Relation(..)
+
+  -- * Construction
+, relation, symmetric_relation, build, buildFrom, buildFromM, identity
+
+  -- * Accessors
+, (!?), (!)
+, bounds, indices, elems, assocs
+, domain, codomain, image, preimage
+
+  -- * Pretty printing
+, table
+)
+where
+
+import Prelude hiding (and, (&&), any)
+import Language.Hasmtlib.Type.MonadSMT
+import Language.Hasmtlib.Type.SMTSort
+import Language.Hasmtlib.Type.Expr
+import Language.Hasmtlib.Boolean
+import Language.Hasmtlib.Codec
+import Data.Coerce
+import Data.Array (Array, Ix(..))
+import Data.Maybe
+import qualified Data.Array as A
+import Control.Monad
+import Control.Lens hiding (indices)
+
+-- | @Relation a b@ represents a binary relation \(R \subseteq A \times B \),
+-- where the domain \(A\) is a finite subset of the type @a@,
+-- and the codomain \(B\) is a finite subset of the type @b@.
+--
+-- A relation is stored internally as @Array (a,b) Expr BoolSort@,
+-- so @a@ and @b@ have to be instances of 'Ix',
+-- and both \(A\) and \(B\) are intervals.
+newtype Relation a b = Relation (Array (a, b) (Expr BoolSort))
+  deriving stock Show
+
+instance (Ix a, Ix b) => Codec (Relation a b) where
+  type Decoded (Relation a b) = Array (a, b) Bool
+  decode s (Relation x) = decode s x
+  encode x = Relation $ encode x
+
+instance (Ix a, Ix b, a ~ c, b ~ d) => Each (Relation a b) (Relation c d) (Expr BoolSort) (Expr BoolSort) where
+  each f (Relation arr) = coerce <$> each f arr
+  {-# INLINE each #-}
+
+type instance Index (Relation a b) = (a,b)
+type instance IxValue (Relation a b) = Expr BoolSort
+instance (Ix a, Ix b) => Ixed (Relation a b) where
+  ix i f (Relation arr) = coerce <$> ix i f arr
+  {-# INLINE ix #-}
+
+-- | @relation ((amin,bmin),(amax,mbax))@ constructs an indeterminate relation \(R \subseteq A \times B \)
+-- where \(A\) is @{amin .. amax}@ and \(B\) is @{bmin .. bmax}@.
+relation :: (Ix a, Ix b, MonadSMT s m) =>
+  ((a,b),(a,b))
+  -> m (Relation a b)
+relation bnd = do
+    pairs <- sequence $ do
+        p <- A.range bnd
+        return $ do
+            x <- var
+            return (p, x)
+    return $ build bnd pairs
+
+-- | Constructs an indeterminate relation \(R \subseteq B \times B \)
+-- that is symmetric, i.e., \(\forall x, y \in B: ((x,y) \in R) \rightarrow ((y,x) \in R) \).
+symmetric_relation ::
+  (MonadSMT s m, Ix b) =>
+  ((b, b), (b, b)) -- ^ Since a symmetric relation must be homogeneous, the domain must equal the codomain.
+                   -- Therefore, given bounds @((p,q),(r,s))@, it must hold that @p=q@ and @r=s@.
+  -> m (Relation b b)
+symmetric_relation bnd = do
+    pairs <- sequence $ do
+        (p,q) <- A.range bnd
+        guard $ p <= q
+        return $ do
+            x <- var
+            return $   ((p,q), x)
+                   : [ ((q,p), x) | p /= q ]
+    return $ build bnd $ concat pairs
+
+-- | Constructs a relation \(R \subseteq A \times B \) from a list.
+build :: (Ix a, Ix b)
+      => ((a,b),(a,b))
+      -> [((a,b), Expr BoolSort)] -- ^ A list of tuples, where the first element represents an element
+                           -- \((x,y) \in A \times B \) and the second element is a positive 'Expr' 'BoolSort'
+                           -- if \((x,y) \in R \), or a negative 'Expr' 'BoolSort' if \((x,y) \notin R \).
+      -> Relation a b
+build bnd pairs = Relation $ A.array bnd pairs
+
+-- | Constructs a relation \(R \subseteq A \times B \) from a function.
+buildFrom :: (Ix a, Ix b)
+          => ((a,b),(a,b))
+          -> ((a,b) -> Expr BoolSort) -- ^ A function that assigns a 'Expr' 'BoolSort'-value to each element \((x,y) \in A \times B \).
+          -> Relation a b
+buildFrom bnd p = build bnd $ flip map (A.range bnd) $ \ i -> (i, p i)
+
+-- | Constructs an indeterminate relation \(R \subseteq A \times B\) from a function.
+buildFromM :: (Ix a, Ix b, MonadSMT s m)
+          => ((a,b),(a,b))
+          -> ((a,b) -> m (Expr BoolSort))
+          -> m (Relation a b)
+buildFromM bnd p = do
+    pairs <- sequence $ do
+        i <- A.range bnd
+        return $ do
+            x <- p i
+            return (i, x)
+    return $ build bnd pairs
+
+-- | Constructs the identity relation \(I = \{ (x,x) ~|~ x \in A \} \subseteq A \times A\).
+identity :: (Ix a)
+         => ((a,a),(a,a)) -- ^ Since the identity relation is homogeneous, the domain must equal the codomain.
+                          -- Therefore, given bounds @((p,q),(r,s))@, it must hold that @p=q@ and @r=s@.
+         -> Relation a a
+identity ((a,b),(c,d))
+    | (a,c) == (b,d) = buildFrom ((a,b),(c,d)) (\ (i,j) -> bool $ i == j)
+    | otherwise      = error "The domain must equal the codomain!"
+
+-- | The bounds of the array that correspond to the matrix representation of the given relation.
+bounds :: Relation a b -> ((a,b),(a,b))
+bounds (Relation r) = A.bounds r
+{-# INLINE bounds #-}
+
+-- | The list of indices, where each index represents an element \((x,y) \in A \times B \)
+-- that may be contained in the given relation \(R \subseteq A \times B \).
+indices :: (Ix a, Ix b) => Relation a b -> [(a, b)]
+indices (Relation r) = A.indices r
+{-# INLINE indices #-}
+
+-- | The list of tuples for the given relation \(R \subseteq A \times B \),
+-- where the first element represents an element \((x,y) \in A \times B \)
+-- and the second element indicates via a 'Expr' 'BoolSort' , if \((x,y) \in R \) or not.
+assocs :: (Ix a, Ix b) => Relation a b -> [((a, b), Expr BoolSort)]
+assocs (Relation r) = A.assocs r
+{-# INLINE assocs #-}
+
+-- | The list of elements of the array
+-- that correspond to the matrix representation of the given relation.
+elems :: Relation a b -> [Expr BoolSort]
+elems (Relation r) = A.elems r
+{-# INLINE elems #-}
+
+-- | 'Maybe' ('Expr' 'BoolSort') for a given element \((x,y) \in A \times B \)
+-- and a given relation \(R \subseteq A \times B \) that indicates
+-- if \((x,y) \in R \) or not.
+--
+-- 'Just' if given element is in 'bounds' of the relation.
+-- 'Nothing' otherwise.
+(!?) :: (Ix a, Ix b) => Relation a b -> (a, b) -> Maybe (Expr BoolSort)
+Relation r !? p = r^?ix p
+{-# INLINE (!?) #-}
+
+-- | Unsafe version of '(!?)'.
+-- Produces an array-indexing-error if given element is not within the 'bounds' of the relation.
+(!) :: (Ix a, Ix b) => Relation a b -> (a, b) -> Expr BoolSort
+Relation r ! p = r A.! p
+{-# INLINE (!) #-}
+
+-- | The domain \(A\) of a relation \(R \subseteq A \times B\).
+domain :: Ix a => Relation a b -> [a]
+domain r =
+  let ((x,_),(x',_)) = bounds r
+  in A.range (x,x')
+{-# INLINE domain #-}
+
+-- | The codomain \(B\) of a relation \(R \subseteq A \times B\).
+codomain :: Ix b => Relation a b -> [b]
+codomain r =
+  let ((_,y),(_,y')) = bounds r
+  in A.range (y,y')
+{-# INLINE codomain #-}
+
+-- | Returns a list of 'Expr' 'BoolSort' indicating whether the projection on
+-- given element \( x \in A \) holds for every element in the codomain:
+--
+-- \( \{ (x,y) \in R \mid y \in codomain(B) \} \)
+image :: (Ix a, Ix b) => Relation a b -> a -> [Expr BoolSort]
+image r x = mapMaybe ((r !?) . (x,)) (codomain r)
+{-# INLINE image #-}
+
+-- | Returns a list of 'Expr' 'BoolSort' indicating whether the projection on
+-- given element \( y \in B \) holds for every element in the domain:
+--
+-- \( \{ (x,y) \in R \mid x \in domain(A) \} \)
+preimage :: (Ix a, Ix b) => Relation a b -> b -> [Expr BoolSort]
+preimage r y = mapMaybe ((r !?) . (,y)) (domain r)
+{-# INLINE preimage #-}
+
+-- | Print a satisfying assignment from an SMT solver, where the assignment is interpreted as a relation.
+-- @putStrLn $ table \</assignment/\>@ corresponds to the matrix representation of this relation.
+table :: (Ix a, Ix b)
+      => Array (a,b) Bool -> String
+table r = unlines $ do
+    let ((a,b),(c,d)) = A.bounds r
+    x <- A.range (a,c)
+    return $ unwords $ do
+        y <- A.range (b,d)
+        return $ if r A.! (x,y) then "*" else "."
diff --git a/src/Language/Hasmtlib/Type/SMT.hs b/src/Language/Hasmtlib/Type/SMT.hs
--- a/src/Language/Hasmtlib/Type/SMT.hs
+++ b/src/Language/Hasmtlib/Type/SMT.hs
@@ -1,7 +1,23 @@
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE UndecidableInstances #-}
 
-module Language.Hasmtlib.Type.SMT where
+{- |
+This module provides a concrete implementation for 'MonadSMT' with it's state 'SMT'.
+-}
+module Language.Hasmtlib.Type.SMT
+(
+  -- * Type
+  SMT(..)
+
+  -- * Lens
+, lastVarId, vars, formulas
+, mlogic, options
+, sharingMode, Language.Hasmtlib.Type.SMT.stableMap
+
+  -- * Rendering
+, renderSetLogic, renderDeclareVar, renderAssert, renderVars
+)
+where
 
 import Language.Hasmtlib.Internal.Sharing
 import Language.Hasmtlib.Internal.Render
diff --git a/src/Language/Hasmtlib/Type/SMTSort.hs b/src/Language/Hasmtlib/Type/SMTSort.hs
--- a/src/Language/Hasmtlib/Type/SMTSort.hs
+++ b/src/Language/Hasmtlib/Type/SMTSort.hs
@@ -2,7 +2,26 @@
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE QuantifiedConstraints #-}
 
-module Language.Hasmtlib.Type.SMTSort where
+{- |
+This module provides the data-type 'SMTSort' and some singleton-operations for it.
+
+The type 'SMTSort' is only used as promoted type (data-kind) in dependent-like contexts such as GADTs.
+-}
+module Language.Hasmtlib.Type.SMTSort
+(
+  -- * Type
+  SMTSort(..)
+, HaskellType
+
+  -- * Singleton
+, SSMTSort(..)
+, KnownSMTSort(..), sortSing'
+
+  -- * Existential
+, SomeSMTSort(..)
+, SomeKnownSMTSort
+)
+where
 
 import Language.Hasmtlib.Internal.Constraint
 import Language.Hasmtlib.Type.Bitvec
diff --git a/src/Language/Hasmtlib/Type/Solution.hs b/src/Language/Hasmtlib/Type/Solution.hs
--- a/src/Language/Hasmtlib/Type/Solution.hs
+++ b/src/Language/Hasmtlib/Type/Solution.hs
@@ -3,9 +3,37 @@
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE UndecidableInstances #-}
 
-module Language.Hasmtlib.Type.Solution where
+{- |
+This module provides the types 'Solution' and 'Result'.
 
+External SMT-Solvers responses are parsed into these types.
+-}
+module Language.Hasmtlib.Type.Solution
+(
+  -- * Solver
+  Solver, Result(..)
+
+  -- * Solution
+, Solution
+, OrdHaskellType
+, SomeKnownOrdSMTSort
+, fromSomeVarSols
+
+  -- ** IntValueMap
+, IntValueMap(..)
+
+  -- ** SMTVarVol
+  -- *** Type
+, SMTVarSol(..)
+
+  -- *** Lens
+, solVar, solVal
+
+)
+where
+
 import Language.Hasmtlib.Type.Expr
+import Language.Hasmtlib.Type.Value
 import Language.Hasmtlib.Type.SMTSort
 import Data.IntMap as IMap hiding (foldl)
 import Data.Dependent.Map as DMap
@@ -18,7 +46,6 @@
 -- | Results of check-sat commands.
 data Result = Unsat | Unknown | Sat deriving (Show, Eq, Ord)
 
--- | A Solution is a dependent map 'DMap' from 'SSMTSort's t to 'IntMap' t.
 type Solution = DMap SSMTSort IntValueMap
 
 -- | Newtype for 'IntMap' 'Value' so we can use it as right-hand-side of 'DMap'.
diff --git a/src/Language/Hasmtlib/Type/Solver.hs b/src/Language/Hasmtlib/Type/Solver.hs
--- a/src/Language/Hasmtlib/Type/Solver.hs
+++ b/src/Language/Hasmtlib/Type/Solver.hs
@@ -1,8 +1,21 @@
+{- |
+This module provides functions for having SMT-Problems solved by external solvers.
+-}
 module Language.Hasmtlib.Type.Solver
-  ( WithSolver(..)
+  (
+  -- * WithSolver
+  WithSolver(..)
+
+  -- * Stateful solving
   , solveWith
+
+  -- * Interactive solving
   , interactiveWith, debugInteractiveWith
+
+  -- ** Minimzation
   , solveMinimized, solveMinimizedDebug
+
+  -- ** Maximization
   , solveMaximized, solveMaximizedDebug
   )
 where
@@ -21,7 +34,7 @@
 
 -- | Data that can have a 'Backend.Solver' which may be debugged.
 class WithSolver a where
-  -- | Create a datum with a 'Backend.Solver' and a 'Bool for whether to debug the 'Backend.Solver'.
+  -- | Create a value with a 'Backend.Solver' and a 'Bool' for whether to debug the 'Backend.Solver'.
   withSolver :: Backend.Solver -> Bool -> a
 
 instance WithSolver Pipe where
@@ -38,7 +51,7 @@
 --    that this answer is only meaningful if the 'Result' is 'Sat' or 'Unknown' and
 --    the answer value is in a 'Just'.
 --
--- Here is a small example of how to use 'solveWith':
+-- ==== __Example__
 --
 -- @
 -- import Language.Hasmtlib
@@ -48,7 +61,7 @@
 --   res <- solveWith @SMT (solver cvc5) $ do
 --     setLogic \"QF_LIA\"
 --
---     x <- var @IntSort
+--     x <- var \@IntSort
 --
 --     assert $ x >? 0
 --
@@ -56,6 +69,8 @@
 --
 --   print res
 -- @
+--
+-- The solver will probably answer with @x := 1@.
 solveWith :: (Default s, Monad m, Codec a) => Solver s m -> StateT s m a -> m (Result, Maybe (Decoded a))
 solveWith solver m = do
   (a, problem) <- runStateT m def
@@ -64,9 +79,9 @@
   return (result, decode solution a)
 
 -- | Pipes an SMT-problem interactively to the solver.
---   Enables incremental solving by default.
---   Here is a small example of how to use it for solving a problem utilizing the solvers incremental stack:
 --
+-- ==== __Example__
+--
 -- @
 -- import Language.Hasmtlib
 -- import Control.Monad.IO.Class
@@ -77,9 +92,9 @@
 --   interactiveWith @Pipe cvc5Living $ do
 --     setOption $ Incremental True
 --     setOption $ ProduceModels True
---     setLogic \"QF_LIA\"
+--     setLogic \"QF_LRA\"
 --
---     x <- var @IntSort
+--     x <- var \@RealSort
 --
 --     assert $ x >? 0
 --
@@ -88,7 +103,7 @@
 --     liftIO $ print $ decode sol x
 --
 --     push
---     y <- var @IntSort
+--     y <- var \@IntSort
 --
 --     assert $ y <? 0
 --     assert $ x === y
@@ -115,8 +130,7 @@
 
 -- | Solves the current problem with respect to a minimal solution for a given numerical expression.
 --
---   Does not rely on MaxSMT/OMT.
---   Instead uses iterative refinement.
+--   Uses iterative refinement.
 --
 --   If you want access to intermediate results, use 'solveMinimizedDebug' instead.
 solveMinimized :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t))
@@ -133,8 +147,7 @@
 
 -- | Solves the current problem with respect to a maximal solution for a given numerical expression.
 --
---   Does not rely on MaxSMT/OMT.
---   Instead uses iterative refinement.
+--   Uses iterative refinement.
 --
 --   If you want access to intermediate results, use 'solveMaximizedDebug' instead.
 solveMaximized :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t))
diff --git a/src/Language/Hasmtlib/Type/Value.hs b/src/Language/Hasmtlib/Type/Value.hs
--- a/src/Language/Hasmtlib/Type/Value.hs
+++ b/src/Language/Hasmtlib/Type/Value.hs
@@ -1,7 +1,18 @@
 {-# LANGUAGE UndecidableInstances #-}
 
+{- |
+This module provides the wrapper 'Value' for embedding Haskell-Values into the SMT-Context.
+
+The Direction @Haskell-Value => SMT-Value@ is the creation of a constant in the SMT-Problem.
+
+The other way around @SMT-Value => Haskell-Value@ is mainly used when decoding a solvers solutions for variables.
+-}
 module Language.Hasmtlib.Type.Value
-( Value(..)
+(
+  -- * Type
+  Value(..)
+
+  -- * Conversion
 , wrapValue, unwrapValue
 )
 where
diff --git a/src/Language/Hasmtlib/Variable.hs b/src/Language/Hasmtlib/Variable.hs
--- a/src/Language/Hasmtlib/Variable.hs
+++ b/src/Language/Hasmtlib/Variable.hs
@@ -1,7 +1,38 @@
 {-# LANGUAGE DefaultSignatures #-}
 
-module Language.Hasmtlib.Variable where
+{- |
+This module provides the class 'Variable' which lets you create symbolical values of a data-type.
 
+A generic default implementation with 'GVariable' is possible.
+
+==== __Example__
+
+@
+data V3 a = V3 a a a deriving Generic
+instance Codec a => Codec (V3 a)
+instance Equatable a => Codec (V3 a)
+
+problem :: MonadSMT s m => StateT s m (V3 (Expr RealSort))
+problem = do
+  let constantV3 = encode $ V3 7 69 42
+  symbolicV3 <- variable \@(V3 (Expr RealSort))
+  assert $ symbolicV3 /== constantV3
+  return symbolicV3
+@
+-}
+module Language.Hasmtlib.Variable
+(
+  -- * Class
+  Variable(..)
+
+  -- * Other functions
+, variable'
+
+  -- * Generics
+, GVariable(..)
+)
+where
+
 import Language.Hasmtlib.Type.Expr
 import Language.Hasmtlib.Type.MonadSMT
 import Language.Hasmtlib.Type.SMTSort
@@ -15,14 +46,6 @@
 -- | Construct a variable datum of a data-type by creating variables for all its fields.
 --
 --   You can derive an instance of this class if your type is 'Generic' and has exactly one constructor.
---
--- @
---    data V3 a = V3 a a a deriving Generic
---    instance Variable a => V3 a
--- @
---
---    >>> varV3 :: V3 (Expr RealType) <- variable ; varV3
---        V3 (Expr RealType) (Expr RealType) (Expr RealType)
 class Variable a where
   variable :: MonadSMT s m => m a
   default variable :: (MonadSMT s m, Generic a, GVariable (Rep a)) => m a