diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -6,6 +6,15 @@
 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.0.1 _(2024-07-23)_
+
+### Added
+- Added more documentation
+
+### Changed
+- `(<==>)` now has `infixr 4`
+- `(<==)` now has `infixl 0`
+
 ## v2.0.0 _(2024-07-23)_
 
 ### Added
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.0.0
+version:               2.0.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.
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
@@ -12,15 +12,15 @@
 import GHC.TypeNats
 
 class Boolean b where
-  -- | Lift a 'Bool'
+  -- | Lift a 'Bool'.
   bool :: Bool -> b
 
-  -- | The true constant
+  -- | The true constant.
   -- @'true' = 'bool' 'True'@
   true :: b
   true = bool True
 
-  -- | The false constant
+  -- | The false constant.
   -- @'false' = 'bool' 'False'@
   false :: b
   false = bool False
@@ -47,16 +47,18 @@
   (<==>) :: b -> b -> b
   x <==> y = (x ==> y) && (y ==> x)
 
-  -- | Logical negation
+  -- | Logical negation.
   not :: b -> b
 
-  -- | Exclusive-or
+  -- | Exclusive-or.
   xor :: b -> b -> b
 
   infix 4 `xor`
+  infixr 4 <==>
   infixr 3 &&
   infixr 2 ||
   infixr 0 ==>
+  infixl 0 <==
 
 -- | The logical conjunction of several values.
 and :: (Foldable t, Boolean b) => t b -> b
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
@@ -20,11 +20,11 @@
 -- | A newtype-wrapper for 'P.Config' which configures a solver via external process.
 newtype ProcessSolver = ProcessSolver { conf :: P.Config }
 
--- | Creates a 'Solver' from a 'ProcessSolver'
+-- | Creates a 'Solver' from a 'ProcessSolver'.
 solver :: (RenderSeq s, MonadIO m) => ProcessSolver -> Solver s m
 solver (ProcessSolver cfg) = processSolver cfg Nothing
 
--- | Creates a debugging 'Solver' from a 'ProcessSolver'
+-- | Creates a debugging 'Solver' from a 'ProcessSolver'.
 debug :: (RenderSeq s, Default (Debugger s), MonadIO m) => ProcessSolver -> Solver s m
 debug (ProcessSolver cfg) = processSolver cfg $ Just def
 
@@ -36,10 +36,10 @@
 
 -- | A type holding actions for debugging states.
 data Debugger s = Debugger
-  { debugState          :: s -> IO ()
-  , debugProblem        :: Seq Builder -> IO ()
-  , debugResultResponse :: ByteString -> IO ()
-  , debugModelResponse  :: ByteString -> IO ()
+  { debugState          :: s -> IO ()               -- ^ Debug the entire state
+  , debugProblem        :: Seq Builder -> IO ()     -- ^ Debug the linewise-rendered problem
+  , debugResultResponse :: ByteString -> IO ()      -- ^ Debug the solvers raw response for @(check-sat)@
+  , debugModelResponse  :: ByteString -> IO ()      -- ^ Debug the solvers raw response for @(get-model)@
   }
 
 instance Default (Debugger SMT) where
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
@@ -20,9 +20,9 @@
 
 -- | An assertion of a booolean expression in OMT that may be weighted.
 data SoftFormula = SoftFormula
-  { _formula  :: Expr BoolSort
-  , _mWeight  :: Maybe Double
-  , _mGroupId :: Maybe String
+  { _formula  :: Expr BoolSort    -- ^ The underlying soft formula
+  , _mWeight  :: Maybe Double     -- ^ Weight of the soft formula
+  , _mGroupId :: Maybe String     -- ^ Group-Id of the soft formula
   } deriving Show
 $(makeLenses ''SoftFormula)