diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,4 +1,4 @@
-![Static Badge](https://img.shields.io/badge/Lang-GHC2021-blue) [![Haskell-CI](https://github.com/bruderj15/Hasmtlib/actions/workflows/haskell-ci.yml/badge.svg)](https://github.com/bruderj15/Hasmtlib/actions/workflows/haskell-ci.yml) [![License: GPL v3](https://img.shields.io/badge/License-GPLv3-blue.svg)](https://www.gnu.org/licenses/gpl-3.0)
+[![Hackage](https://img.shields.io/hackage/v/hasmtlib.svg)](https://hackage.haskell.org/package/hasmtlib) ![Static Badge](https://img.shields.io/badge/Lang-GHC2021-blue) [![Haskell-CI](https://github.com/bruderj15/Hasmtlib/actions/workflows/haskell-ci.yml/badge.svg)](https://github.com/bruderj15/Hasmtlib/actions/workflows/haskell-ci.yml) [![License: GPL v3](https://img.shields.io/badge/License-GPLv3-blue.svg)](https://www.gnu.org/licenses/gpl-3.0)
 
 # Hasmtlib
 
diff --git a/hasmtlib.cabal b/hasmtlib.cabal
--- a/hasmtlib.cabal
+++ b/hasmtlib.cabal
@@ -1,41 +1,12 @@
 cabal-version:         3.0
 
 name:                  hasmtlib
-version:               1.0.0
+version:               1.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.
   It is highly inspired by ekmett/ersatz which does the same for QSAT.
   Communication with external solvers is handled by tweag/smtlib-backends.
-  .
-  For example we can utilize existing instances for V3 to symbolically use Num and Metric operations.
-  .
-  > {-# LANGUAGE DataKinds #-}
-  .
-  > import Language.Hasmtlib
-  > import Linear
-  .
-  > -- instances with default impl
-  > instance Codec a => Codec (V3 a)
-  > instance Variable a => Variable (V3 a)
-  .
-  > main :: IO ()
-  > main = do
-  >   res <- solveWith (solver cvc5) $ do
-  >     setLogic "QF_NRA"
-  >
-  >     u :: V3 (Expr RealSort) <- variable
-  >     v <- variable
-  >
-  >     assert $ dot u v === 5
-  >
-  >     return (u,v)
-  >
-  >   print res
-  .
-  May print:
-  > (Sat,Just (V3 (-2.0) (-1.0) 0.0,V3 (-2.0) (-1.0) 0.0))
 homepage:              https://github.com/bruderj15/Hasmtlib
 license:               GPL-3.0-only
 license-file:          LICENSE
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
@@ -25,7 +25,7 @@
 --    results ('Unknown').
 --
 -- 2. A 'Decoded' answer that was decoded using the solution to @prob@. Note
---    that this answer is only meaningful if the 'Result' is 'Satisfied or Unknown' and
+--    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':