diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,9 @@
+0.4.13 [2022.11.01]
+-------------------
+* Make the examples compile with `mtl-2.3.*`.
+* Add more documentation to the `Ersatz.Relation.*` modules, the `Variable`
+  class, and the data types in `Ersatz.Bits`.
+
 0.4.12 [2022.08.11]
 -------------------
 * Add `Equatable` and `Orderable` instances for more base and containers types
diff --git a/ersatz.cabal b/ersatz.cabal
--- a/ersatz.cabal
+++ b/ersatz.cabal
@@ -1,5 +1,5 @@
 name:           ersatz
-version:        0.4.12
+version:        0.4.13
 license:        BSD3
 license-file:   LICENSE
 author:         Edward A. Kmett, Eric Mertens, Johan Kiviniemi
diff --git a/examples/regexp-grid/RegexpGrid/Problem.hs b/examples/regexp-grid/RegexpGrid/Problem.hs
--- a/examples/regexp-grid/RegexpGrid/Problem.hs
+++ b/examples/regexp-grid/RegexpGrid/Problem.hs
@@ -10,8 +10,11 @@
 
 import Control.Applicative
 import qualified Control.Monad.Fail as Fail
-import Control.Monad.Reader
-import Control.Monad.RWS.Strict hiding ((<>))
+import Control.Monad (guard)
+import Control.Monad.Reader (MonadReader(..), ReaderT(..))
+import Control.Monad.RWS.Strict (RWST, evalRWST)
+import Control.Monad.Trans (MonadTrans(..))
+import Control.Monad.Writer.Strict (MonadWriter(..))
 import Control.Lens
 import qualified Data.Foldable as F (asum)
 import Data.Map (Map)
diff --git a/examples/sudoku/Sudoku/Problem.hs b/examples/sudoku/Sudoku/Problem.hs
--- a/examples/sudoku/Sudoku/Problem.hs
+++ b/examples/sudoku/Sudoku/Problem.hs
@@ -3,7 +3,8 @@
 
 import Prelude hiding ((&&), (||), not, and, or, all, any)
 
-import Control.Monad.Reader
+import Control.Monad (forM_, replicateM, when)
+import Control.Monad.Reader (ReaderT(..), asks)
 import Data.Array (Array, (!))
 import qualified Data.Array as Array
 import Data.Word
diff --git a/src/Ersatz/Bits.hs b/src/Ersatz/Bits.hs
--- a/src/Ersatz/Bits.hs
+++ b/src/Ersatz/Bits.hs
@@ -8,7 +8,17 @@
 -- Stability :  experimental
 -- Portability: non-portable
 --
--- 'Bits' is an arbitrary length natural number type
+-- 'Bit1' .. 'Bit8' represent fixed length bit vectors.
+-- The most significant bit comes first.
+-- 'Bit1' and 'Bit2' have modular arithmetic
+-- (the result has the same width as the arguments, overflow is ignored).
+--
+-- 'Bits' is an arbitrary length natural number type.
+-- The least significant bit comes first.
+-- 'Bits' has full arithmetic
+-- (the result has large enough width so that there is no overflow).
+
+
 --------------------------------------------------------------------
 module Ersatz.Bits
   (
@@ -41,21 +51,21 @@
 import GHC.Generics
 import Prelude hiding (and, or, not, (&&), (||))
 
--- | A container of 1 'Bit' that 'encode's from and 'decode's to 'Word8'
+-- | A container of 1 'Bit' that 'encode's from and 'decode's to 'Word8'.
 newtype Bit1 = Bit1 Bit deriving (Show,Generic)
--- | A container of 2 'Bit's that 'encode's from and 'decode's to 'Word8'
+-- | A container of 2 'Bit's that 'encode's from and 'decode's to 'Word8'. MSB is first.
 data Bit2 = Bit2 !Bit !Bit deriving (Show,Generic)
--- | A container of 3 'Bit's that 'encode's from and 'decode's to 'Word8'
+-- | A container of 3 'Bit's that 'encode's from and 'decode's to 'Word8'. MSB is first.
 data Bit3 = Bit3 !Bit !Bit !Bit deriving (Show,Generic)
--- | A container of 4 'Bit's that 'encode's from and 'decode's to 'Word8'
+-- | A container of 4 'Bit's that 'encode's from and 'decode's to 'Word8'. MSB is first.
 data Bit4 = Bit4 !Bit !Bit !Bit !Bit deriving (Show,Generic)
--- | A container of 5 'Bit's that 'encode's from and 'decode's to 'Word8'
+-- | A container of 5 'Bit's that 'encode's from and 'decode's to 'Word8'. MSB is first.
 data Bit5 = Bit5 !Bit !Bit !Bit !Bit !Bit deriving (Show,Generic)
--- | A container of 6 'Bit's that 'encode's from and 'decode's to 'Word8'
+-- | A container of 6 'Bit's that 'encode's from and 'decode's to 'Word8'. MSB is first.
 data Bit6 = Bit6 !Bit !Bit !Bit !Bit !Bit !Bit deriving (Show,Generic)
--- | A container of 7 'Bit's that 'encode's from and 'decode's to 'Word8'
+-- | A container of 7 'Bit's that 'encode's from and 'decode's to 'Word8'. MSB is first.
 data Bit7 = Bit7 !Bit !Bit !Bit !Bit !Bit !Bit !Bit deriving (Show,Generic)
--- | A container of 8 'Bit's that 'encode's from and 'decode's to 'Word8'
+-- | A container of 8 'Bit's that 'encode's from and 'decode's to 'Word8'. MSB is first.
 data Bit8 = Bit8 !Bit !Bit !Bit !Bit !Bit !Bit !Bit !Bit deriving (Show,Generic)
 
 instance Boolean Bit1
@@ -176,6 +186,8 @@
 boolToNum True  = 1
 {-# INLINE boolToNum #-}
 
+
+-- | This instance provides modular arithmetic (overflow is ignored).
 instance Num Bit1 where
   Bit1 a + Bit1 b = Bit1 (xor a b)
   Bit1 a * Bit1 b = Bit1 (a && b)
@@ -210,6 +222,7 @@
 halfAdder :: Bit -> Bit -> (Bit, Bit) -- ^ (sum, carry)
 halfAdder a b = (a `xor` b, a && b)
 
+-- | This instance provides modular arithmetic (overflow is ignored).
 instance Num Bit2 where
   Bit2 a2 a1 + Bit2 b2 b1 = Bit2 s2 s1 where
     (s1,c2) = halfAdder a1 b1
@@ -231,8 +244,8 @@
   signum (Bit2 a b) = Bit2 false (a || b)
   fromInteger k = Bit2 (bool (k .&. 2 /= 0)) (bool (k .&. 1 /= 0))
 
--- suitable for comparisons and arithmetic. Bits are stored
--- in little-endian order to enable phantom 'false' values
+-- | A container of 'Bit's that is suitable for comparisons and arithmetic. Bits are stored
+-- with least significant bit first to enable phantom 'false' values
 -- to be truncated.
 newtype Bits = Bits { _getBits :: [Bit] }
 
@@ -391,6 +404,16 @@
   times2 = (false:)
   aux x ys = Bits (map (x &&) ys)
 
+-- | This instance provides full arithmetic.
+-- The result has large enough width so that there is no overflow.
+--
+-- Subtraction is modified: @a - b@ denotes @max 0 (a - b)@.
+--
+-- Width of @a + b@ is @1 + max (width a) (width b)@,
+-- width of @a * b@ is @(width a) + (width b)@,
+-- width of @a - b@ is @max (width a) (width b)@.
+--
+-- @fromInteger@ will raise 'error' for negative arguments.
 instance Num Bits where
   (+) = addBits false
   (*) = mulBits
diff --git a/src/Ersatz/Relation.hs b/src/Ersatz/Relation.hs
--- a/src/Ersatz/Relation.hs
+++ b/src/Ersatz/Relation.hs
@@ -1,3 +1,16 @@
+-- | Copyright: Johannes Waldmann, Antonia Swiridoff
+-- License: BSD3
+--
+-- The type @Relation a b@ represents relations
+-- between finite subsets of type @a@ and of type @b@.
+--
+-- A relation is stored internally as @Array (a,b) Bit@,
+-- and some methods of @Data.Array@ are provided for managing indices and elements.
+--
+-- These are rarely needed, because we provide operations and properties
+-- in a point-free style, that is, without reference to individual indices and elements.
+
+
 module Ersatz.Relation
 ( module Ersatz.Relation.Data
 , module Ersatz.Relation.Op
diff --git a/src/Ersatz/Relation/Data.hs b/src/Ersatz/Relation/Data.hs
--- a/src/Ersatz/Relation/Data.hs
+++ b/src/Ersatz/Relation/Data.hs
@@ -1,14 +1,21 @@
 {-# language TypeFamilies #-}
 
-module Ersatz.Relation.Data ( Relation
+module Ersatz.Relation.Data ( 
+-- * The 'Relation' type
+  Relation
+-- * Construction
 , relation, symmetric_relation
 , build
 , buildFrom
 , identity
+-- * Components
 , bounds, (!), indices, assocs, elems
+-- *
 , table
 )  where
 
+import Prelude hiding ( and )
+
 import Ersatz.Bit
 import Ersatz.Codec
 import Ersatz.Variable (exists)
@@ -18,6 +25,15 @@
 import qualified Data.Array as A
 import Data.Array ( Array, Ix )
 
+
+-- | @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) Bit@,
+-- so @a@ and @b@ have to be instances of 'Ix',
+-- and both \(A\) and \(B\) are intervals.
+
 newtype Relation a b = Relation (A.Array (a, b) Bit)
 
 instance (Ix a, Ix b) => Codec (Relation a b) where
@@ -25,8 +41,12 @@
   decode s (Relation a) = decode s a
   encode a = Relation $ encode a
 
-relation :: ( Ix a, Ix b, MonadSAT s m )
-         => ((a,b),(a,b)) -> m ( Relation a b )
+
+-- | @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, MonadSAT s m ) =>
+  ((a,b),(a,b)) 
+  -> m ( Relation a b )
 relation bnd = do
     pairs <- sequence $ do
         p <- A.range bnd
@@ -35,9 +55,15 @@
             return ( p, x )
     return $ build bnd pairs
 
+-- | Constructs an indeterminate relation \( R \subseteq B \times B \)
+-- that it is symmetric, i.e., \( \forall x, y \in B: ((x,y) \in R) \rightarrow ((y,x) \in R) \).
+--
+-- A symmetric relation is an undirected graph, possibly with loops.
 symmetric_relation ::
   (MonadSAT s m, Ix b) =>
-  ((b, b), (b, b)) -> m (Relation b 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
@@ -48,38 +74,98 @@
                    : [ ((q,p), x) | p /= q ]
     return $ build bnd $ concat pairs
 
+-- | Constructs a relation \(R \subseteq A \times B \) from a list.
+-- 
+-- ==== __Example__
+--
+-- @
+-- r = build ((0,'a'),(1,'b')) [((0,'a'), true), ((0,'b'), false), 
+--                          ((1,'a'), false), ((1,'b'), true))]
+-- @
 build :: ( Ix a, Ix b )
       => ((a,b),(a,b))
-      -> [ ((a,b), Bit ) ]
+      -> [ ((a,b), Bit ) ] -- ^ A list of tuples, where the first element represents an element
+                           -- \( (x,y) \in A \times B \) and the second element is a positive 'Bit'
+                           -- if \( (x,y) \in R \), or a negative 'Bit' 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 -> Bit) -> ((a,b),(a,b)) -> Relation a b
-buildFrom p bnd = build bnd $ flip map (A.range bnd) $ \ (i,j) ->
-    ((i,j), p i j)
+          => (a -> b -> Bit) -- ^ A function with the specified signature, that assigns a 'Bit'-value 
+                             -- to each element \( (x,y) \in A \times B \).
+          -> ((a,b),(a,b))
+          -> Relation a b
+buildFrom p bnd = build bnd $ flip map (A.range bnd) $ \ (i,j) -> ((i, j), p i j)
 
+-- | Constructs the identity relation \(I \subseteq A \times A, I = \{ (x,x) ~|~ x \in A \} \).
 identity :: (Ix a)
-         => ((a,a),(a,a)) -> Relation a 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 = buildFrom (\ i j -> bool $ i == j)
 
 
+-- | The bounds of the array that correspond to the matrix representation of the given relation.
+--
+-- ==== __Example__
+--
+-- >>> r = build ((0,0),(1,1)) [((0,0), false), ((0,1), true), ((1,0), true), ((1,1), false))]
+-- >>> bounds r
+-- ((0,0),(1,1))
 bounds :: (Ix a, Ix b) => Relation a b -> ((a,b),(a,b))
 bounds ( Relation r ) = A.bounds r
 
+-- | 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 \).
+--
+-- ==== __Example__
+--
+-- >>> r = build ((0,0),(1,1)) [((0,0), false), ((0,1), true), ((1,0), true), ((1,1), false))]
+-- >>> indices r
+-- [(0,0),(0,1),(1,0),(1,1)]
 indices :: (Ix a, Ix b) => Relation a b -> [(a, b)]
 indices ( Relation r ) = A.indices r
 
+-- | 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 'Bit' , if \( (x,y) \in R \) or not.
+-- 
+-- ==== __Example__
+--
+-- >>> r = build ((0,0),(1,1)) [((0,0), false), ((0,1), true), ((1,0), true), ((1,1), false))]
+-- >>> assocs r
+-- [((0,0),Var (-1)),((0,1),Var 1),((1,0),Var 1),((1,1),Var (-1))]
 assocs :: (Ix a, Ix b) => Relation a b -> [((a, b), Bit)]
 assocs ( Relation r ) = A.assocs r
 
+-- | The list of elements of the array
+-- that correspond to the matrix representation of the given relation.
+--
+-- ==== __Example__
+--
+-- >>> r = build ((0,0),(1,1)) [((0,0), false), ((0,1), true), ((1,0), true), ((1,1), false))]
+-- >>> elems r
+-- [Var (-1),Var 1,Var 1,Var (-1)]
 elems :: (Ix a, Ix b) => Relation a b -> [Bit]
 elems ( Relation r ) = A.elems r
 
+-- | The 'Bit'-value 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.
+-- 
+-- ==== __Example__
+--
+-- >>> r = build ((0,0),(1,1)) [((0,0), false), ((0,1), true), ((1,0), true), ((1,1), false))]
+-- >>> r ! (0,0)
+-- Var (-1)
+-- >>> r ! (0,1)
+-- Var 1
 (!) :: (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
 Relation r ! p = r A.! p
 
-
+-- | Print a satisfying assignment from a SAT solver, where the assignment is interpreted as a relation.
+-- @putStrLn $ table \</assignment/\>@ corresponds to the matrix representation of this relation.
 table :: (Enum a, Ix a, Enum b, Ix b)
       => Array (a,b) Bool -> String
 table r = unlines $ do
diff --git a/src/Ersatz/Relation/Op.hs b/src/Ersatz/Relation/Op.hs
--- a/src/Ersatz/Relation/Op.hs
+++ b/src/Ersatz/Relation/Op.hs
@@ -2,7 +2,9 @@
 
 module Ersatz.Relation.Op
 
-( mirror
+( 
+-- * Operations
+  mirror
 , union
 , complement
 , difference
@@ -21,26 +23,45 @@
 
 import Data.Ix
 
+-- | Constructs the converse relation \( R^{-1} \subseteq B \times A \) of a relation 
+-- \( R \subseteq A \times B \), which is defined by \( R^{-1} = \{ (y,x) ~|~ (x,y) \in R \} \).
 mirror :: ( Ix a , Ix b ) => Relation a b -> Relation b a
 mirror r =
     let ((a,b),(c,d)) = bounds r
     in  build ((b,a),(d,c)) $ do (x,y) <- indices r ; return ((y,x), r!(x,y))
 
+-- | Constructs the complement relation \( \overline{R} \) 
+-- of a relation \( R \subseteq A \times B \), which is defined by 
+-- \( \overline{R}  = \{ (x,y) \in A \times B ~|~ (x,y) \notin R \} \).
 complement :: ( Ix a , Ix b ) => Relation a b -> Relation a b
 complement r =
     build (bounds r) $ do i <- indices r ; return ( i, not $ r!i )
 
+-- | Constructs the difference \( R \setminus S \) of the relations 
+-- \(R\) and \(S\), that contains all elements that are in \(R\) but not in \(S\), i.e.,
+-- \( R \setminus S = \{ (x,y) \in R ~|~ (x,y) \notin S \} \).
+--
+-- Note that if \( R \subseteq A \times B \) and \( S \subseteq C \times D \),
+-- then \( A \times B \) must be a subset of \( C \times D \) and
+-- \( R \setminus S \subseteq A \times B \).
 difference :: ( Ix a , Ix b )
         => Relation a b -> Relation a b ->  Relation a b
 difference r s =
     intersection r $ complement s
 
+-- | Constructs the union \( R \cup S \) of the relations \( R \) and \( S \).
+--
+-- Note that for \( R \subseteq A \times B \) and \( S \subseteq C \times D \),
+-- it must hold that \( A \times B \subseteq C \times D \).
 union :: ( Ix a , Ix b )
         => Relation a b -> Relation a b ->  Relation a b
 union r s =  build ( bounds r ) $ do
     i <- indices r
     return (i, or [ r!i, s!i ] )
 
+-- | Constructs the composition \( R \cdot S \) of the relations 
+-- \( R \subseteq A \times B \) and \( S \subseteq B \times C \), which is 
+-- defined by \( R \cdot S = \{ (a,c) ~|~ ((a,b) \in R) \land ((b,c) \in S) \} \).
 product :: ( Ix a , Ix b, Ix c )
         => Relation a b -> Relation b c ->  Relation a c
 product a b =
@@ -54,8 +75,13 @@
                 return $ and [ a!(x,y), b!(y,z) ]
                 )
 
+-- | Constructs the relation \( R^{n} \) that results if a relation
+-- \( R \subseteq A \times A \) is composed \(n\) times with itself.
+--
+-- \( R^{0} \) is the identity relation \( I_{R} = \{ (x,x) ~|~ x \in A \} \) of \(R\).
 power  :: ( Ix a  )
-        => Int -> Relation a a -> Relation a a
+        => Int -- ^ \(n\)
+        -> Relation a a -> Relation a a
 power 0 r = identity ( bounds r )
 power 1 r = r
 power e r =
@@ -66,6 +92,10 @@
         0 -> s2
         _ -> product s2 r
 
+-- | Constructs the intersection \( R \cap S \) of the relations \( R \) and \( S \).
+--
+-- Note that for \( R \subseteq A \times B \) and \( S \subseteq C \times D \),
+-- it must hold that \( A \times B \subseteq C \times D \).
 intersection :: ( Ix a , Ix b)
       => Relation a b -> Relation a b
       -> Relation a b
@@ -73,10 +103,16 @@
         i <- indices r
         return (i, and [ r!i, s!i ] )
 
+-- | Constructs the reflexive closure \( R \cup I_{R} \) of the relation 
+-- \( R \subseteq A \times A \), where \( I_{R} = \{ (x,x) ~|~ x \in A \} \) 
+-- is the identity relation of \(R\).
 reflexive_closure :: Ix a => Relation a a -> Relation a a
 reflexive_closure t =
     union t $ identity $ bounds t
 
+-- | Constructs the symmetric closure \( R \cup R^{-1} \) of the relation 
+-- \( R \subseteq A \times A \), where \( R^{-1} = \{ (y,x) ~|~ (x,y) \in R \} \)
+-- is converse relation of \(R\).
 symmetric_closure :: Ix a => Relation a a -> Relation a a
 symmetric_closure r =
     union r $ mirror r
diff --git a/src/Ersatz/Relation/Prop.hs b/src/Ersatz/Relation/Prop.hs
--- a/src/Ersatz/Relation/Prop.hs
+++ b/src/Ersatz/Relation/Prop.hs
@@ -1,7 +1,8 @@
-
 module Ersatz.Relation.Prop
 
-( implies
+( 
+-- * Properties
+  implies
 , symmetric
 , anti_symmetric
 , transitive
@@ -31,50 +32,100 @@
 
 import Data.Ix
 
+-- | Tests if the first relation \(R\) is a subset of the second relation \(S\), 
+-- i.e., every element that is contained in \(R\) is also contained in \(S\).
+--
+-- Note that if \( R \subseteq A \times B \) and \( S \subseteq C \times D \),
+-- then \( A \times B \) must be a subset of \( C \times D \).
 implies :: ( Ix a, Ix b )
         => Relation a b -> Relation a b -> Bit
 implies r s = and $ do
     i <- indices r
     return $ or [ not $ r ! i, s ! i ]
 
+-- | Tests if a relation is empty, i.e., the relation doesn't contain any elements.
 empty ::  ( Ix a, Ix b )
         => Relation a b -> Bit
 empty r = and $ do
     i <- indices r
     return $ not $ r ! i
 
+-- | Tests if a relation \( R \subseteq A \times B \) is complete,
+-- i.e., \(R = A \times B \).
 complete :: (Ix a, Ix b) => Relation a b -> Bit
 complete r = empty $ complement r
 
+-- | Tests if a relation \( R \subseteq A \times A \) is strongly connected, i.e.,
+-- \( \forall x, y \in A: ((x,y) \in R) \lor ((y,x) \in R) \).
 total :: ( Ix a) => Relation a a -> Bit
 total r = complete $ symmetric_closure r
 
+-- | Tests if two relations are disjoint, i.e., 
+-- there is no element that is contained in both relations.
 disjoint :: (Ix a, Ix b) => Relation a b -> Relation a b -> Bit
 disjoint r s = empty $ intersection r s
 
+-- | Tests if two relations \( R, S \subseteq A \times B \) are equal, 
+-- i.e., they contain the same elements.
 equals :: (Ix a, Ix b) => Relation a b -> Relation a b -> Bit
 equals r s = and [implies r s, implies s r]
 
+-- | Tests if a relation \( R \subseteq A \times A \) is symmetric,
+-- i.e., \( \forall x, y \in A: ((x,y) \in R) \rightarrow ((y,x) \in R) \).
 symmetric :: ( Ix a) => Relation a a -> Bit
 symmetric r = implies r ( mirror r )
 
+
+-- | Tests if a relation \( R \subseteq A \times A \) is antisymmetric,
+-- i.e., \( \forall x, y \in A: ((x,y) \in R) \land ((y,x) \in R)) \rightarrow (x = y) \).
 anti_symmetric :: ( Ix a) => Relation a a -> Bit
 anti_symmetric r = implies (intersection r (mirror r)) (identity (bounds r))
 
+-- | Tests if a relation \( R \subseteq A \times A \) is irreflexive, i.e.,
+-- \( \forall x \in A: (x,x) \notin R \).
 irreflexive :: ( Ix a ) => Relation a a -> Bit
 irreflexive r = and $ do
     let ((a,_),(c,_)) = bounds r
     x <- range (a, c)
     return $ not $ r ! (x,x)
 
+-- | Tests if a relation \( R \subseteq A \times A \) is reflexive, i.e.,
+-- \( \forall x \in A: (x,x) \in R \).
 reflexive :: ( Ix a ) => Relation a a -> Bit
 reflexive r = and $ do
     let ((a,_),(c,_)) = bounds r
     x <- range (a,c)
     return $ r ! (x,x)
 
-regular, regular_in_degree, regular_out_degree, max_in_degree, min_in_degree, max_out_degree, min_out_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit
+-- | Given an 'Int' \( n \) and a relation \( R \subseteq A \times B \), check if
+-- \( \forall x \in A: | \{ (x,y) \in R \} | = n \) and
+-- \( \forall y \in B: | \{ (x,y) \in R \} | = n \) hold.
+regular :: (Ix a, Ix b) => Int -> Relation a b -> Bit
 
+-- | Given an 'Int' \( n \) and a relation \( R \subseteq A \times B \), check if
+-- \( \forall y \in B: | \{ (x,y) \in R \} | = n \) holds.
+regular_in_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit
+
+-- | Given an 'Int' \( n \) and a relation \( R \subseteq A \times B \), check if
+-- \( \forall x \in A: | \{ (x,y) \in R \} | = n \) holds.
+regular_out_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit
+
+-- | Given an 'Int' \( n \) and a relation \( R \subseteq A \times B \), check if
+-- \( \forall y \in B: | \{ (x,y) \in R \} | \leq n \) holds.
+max_in_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit
+
+-- | Given an 'Int' \( n \) and a relation \( R \subseteq A \times B \), check if
+-- \( \forall y \in B: | \{ (x,y) \in R \} | \geq n \) holds.
+min_in_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit
+
+-- | Given an 'Int' \( n \) and a relation \( R \subseteq A \times B \), check if
+-- \( \forall x \in A: | \{ (x,y) \in R \} | \leq n \) holds.
+max_out_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit
+
+-- | Given an 'Int' \( n \) and a relation \( R \subseteq A \times B \), check if
+-- \( \forall x \in A: | \{ (x,y) \in R \} | \geq n \) holds.
+min_out_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit
+
 regular deg r = and [ regular_in_degree deg r, regular_out_degree deg r ]
 
 regular_out_degree = out_degree_helper exactly
@@ -94,6 +145,8 @@
         y <- range (b,d)
         return $ r ! (x,y)
 
+-- | Tests if a relation \( R \subseteq A \times A \) is transitive, i.e.,
+-- \( \forall x, y \in A: ((x,y) \in R) \land ((y,z) \in R) \rightarrow ((x,z) \in R) \).
 transitive :: ( Ix a )
            => Relation a a -> Bit
 transitive r = implies (product r r) r
diff --git a/src/Ersatz/Variable.hs b/src/Ersatz/Variable.hs
--- a/src/Ersatz/Variable.hs
+++ b/src/Ersatz/Variable.hs
@@ -51,8 +51,26 @@
 instance GVariable f => GVariable (M1 i c f) where
   gliterally = fmap M1 . gliterally
 
--- | Instances for this class for product-like types can be automatically derived
+-- | This class describes all types that can be represented
+-- by a collection of literals. The class method 'literally'
+-- is usually applied to 'literalExists' or 'literalForall',
+-- see implementations of 'exists' and 'forall'.
+--
+-- Instances for this class for product-like types can be automatically derived
 -- for any type that is an instance of 'Generic'.
+--
+-- === __Example usage__
+--
+-- @
+-- {-# language DeriveGeneric, TypeApplications #-}
+-- import GHC.Generics
+--
+-- data T = C Bit Bit deriving Generic
+-- instance Variable T
+--
+-- constraint = do t <- exists @T ; ...
+-- @
+
 class Variable t where
   literally :: MonadSAT s m => m Literal -> m t
   default literally ::