diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -16,15 +16,16 @@
 {-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE DeriveFoldable #-}
 {-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE DerivingVia #-}
 
 import Control.Monad (ap)
 import Bound.Simple (Scope, Bound(..), abstract1, instantiate1)
+import Data.Functor.Classes (Show1)
 import Data.Functor.Classes.Generic (Generically(..))
-
 import GHC.Generics (Generic1)
 
-infixl 9 :
-data Exp a = V a | Exp a : Exp a | Lam (Scope () Exp a)
+infixl 9 :@
+data Exp a = V a | Exp a :@ Exp a | Lam (Scope () Exp a)
   deriving (Show, Functor, Foldable, Traversable, Generic1)
   deriving (Show1) via Generically Exp
 
diff --git a/bound-simple.cabal b/bound-simple.cabal
--- a/bound-simple.cabal
+++ b/bound-simple.cabal
@@ -1,5 +1,5 @@
 name:                bound-simple
-version:             0.1.0.0
+version:             0.2.0.0
 synopsis:            A lightweight implementation of 'bound'
 description:         An abstraction for representing bound variables. Most of this code has been extracted from 'bound', with the purpose of providing a mostly self-contained library for implementing embedded languages.
 homepage:            https://github.com/ocramz/bound-simple
diff --git a/src/Bound/Simple.hs b/src/Bound/Simple.hs
--- a/src/Bound/Simple.hs
+++ b/src/Bound/Simple.hs
@@ -7,67 +7,60 @@
 {-# LANGUAGE DeriveFunctor #-}
 {-# language CPP #-}
 {-# options_ghc -Wno-unused-top-binds #-}
------------------------------------------------------------------------------
--- |
--- Copyright   :  (C) 2013 Edward Kmett
---                (C) 2021 Marco Zocca (ocramz)
--- License     :  BSD-style (see the file LICENSE)
---
--- Maintainer  :  ocramz
--- Stability   :  experimental
--- Portability :  portable
---
--- 'Scope' is to be used inside of the definition of binders.
---
--- A lightweight implementation of 'bound'. Provides much of the functionality of Bound.Scope.Simple, without the large dependency footprint.
---
--- = Example
---
--- The 'whnf' function in this example shows how to beta-reduce a term of the untyped lambda calculus.
---
--- Note : the Show instance of Exp depends on its Show1 instance (since Exp has one type parameter), which can be derived 'Generically' thanks to DerivingVia. This works on most recent versions of GHC (>= 8.6.1).
---
--- @
--- {-# LANGUAGE DeriveFunctor #-}
--- {-# LANGUAGE DeriveFoldable #-}
--- {-# LANGUAGE DeriveTraversable #-}
---
--- import Bound.Simple (Scope, Bound(..), abstract1, instantiate1)
--- import Data.Functor.Classes.Generic (Generically(..))
--- 
--- import GHC.Generics (Generic1)
---
--- infixl 9 :\@
--- data Exp a = V a | Exp a :@ Exp a | Lam (Scope () Exp a)
---   deriving (Show, Functor, Foldable, Traversable, Generic1)
---   deriving (Show1) via Generically Exp
---
--- instance Applicative Exp where pure = V; k \<*\> m = ap k m
---
--- instance Monad Exp where
---   return = V
---   V a      >>= f = f a
---   (x :\@ y) >>= f = (x >>= f) :\@ (y >>= f)
---   Lam e    >>= f = Lam (e '>>>=' f)
---
--- lam :: Eq a => a -> Exp a -> Exp a
--- lam v b = Lam ('abstract1' v b)
---
--- whnf :: Exp a -> Exp a
--- whnf (e1 \:\@ e2) = case whnf e1 of
---   Lam b -> whnf ('instantiate1' e2 b)
---   f'    -> f' :\@ e2
--- whnf e = e
---
--- main :: IO ()
--- main = do
---   let term = lam 'x' (V 'x') :\@ V 'y'
---   print term         -- Lam (Scope (V (B ()))) :\@ V 'y'
---   print $ whnf term  -- V 'y'
--- @
-----------------------------------------------------------------------------
 
+{-|
+Module      : Bound.Simple
+Description : Lightweight implementation of 'bound'
+Copyright   : (c) 2013 Edward Kmett, 2021 Marco Zocca
+License     : BSD
+Maintainer  : github.com/ocramz
+Stability   : experimental
+Portability : POSIX
 
+= Example
+
+The 'whnf' function in this example shows how to beta-reduce a term of the untyped lambda calculus.
+
+Note : the Show instance of Exp depends on its Show1 instance (since Exp has one type parameter), which can be derived 'Generically'. This works on most recent versions of GHC (>= 8.6.1).
+
+Note 2 : the example below requires language extensions `DeriveFunctor`, `DeriveFoldable`, `DeriveTraversable` and `DerivingVia`.
+
+@
+import Bound.Simple (Scope, Bound(..), abstract1, instantiate1)
+import Data.Functor.Classes (Show1)
+import Data.Functor.Classes.Generic (Generically(..))
+
+import GHC.Generics (Generic1)
+
+infixl 9 :\@
+data Exp a = V a | Exp a :@ Exp a | Lam (Scope () Exp a)
+  deriving (Show, Functor, Foldable, Traversable, Generic1)
+  deriving (Show1) via Generically Exp
+
+instance Applicative Exp where pure = V; k \<*\> m = ap k m
+
+instance Monad Exp where
+  return = V
+  V a      >>= f = f a
+  (x :\@ y) >>= f = (x >>= f) :\@ (y >>= f)
+  Lam e    >>= f = Lam (e '>>>=' f)
+
+lam :: Eq a => a -> Exp a -> Exp a
+lam v b = Lam ('abstract1' v b)
+
+whnf :: Exp a -> Exp a
+whnf (e1 \:\@ e2) = case whnf e1 of
+  Lam b -> whnf ('instantiate1' e2 b)
+  f'    -> f' :\@ e2
+whnf e = e
+
+main :: IO ()
+main = do
+  let term = lam 'x' (V 'x') :\@ V 'y'
+  print term         -- Lam (Scope (V (B ()))) :\@ V 'y'
+  print $ whnf term  -- V 'y'
+@
+-}
 module Bound.Simple (Bound(..)
                     , Scope, toScope, fromScope
                     , Var
@@ -91,6 +84,10 @@
 import Data.Functor.Classes (Show2(..), Show1(..), showsUnaryWith, showsPrec1, liftShowsPrec2, Eq2(..), Eq1(..), eq1, liftEq, liftEq2)
 import GHC.Generics (Generic1)
 import Data.Functor.Classes.Generic (Generically(..))
+
+
+
+
 
 infixl 9 :@
 data Exp a = V a | Exp a :@ Exp a | Lam (Scope () Exp a)