diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.markdown
@@ -0,0 +1,7 @@
+0.5
+-----
+* Created a `doctest`-based test suite
+* Added many examples
+* 100% haddock coverage
+* Added the `Name` `Comonad`, to help retain names for bound variables.
+* Bumped dependencies
diff --git a/bound.cabal b/bound.cabal
--- a/bound.cabal
+++ b/bound.cabal
@@ -1,6 +1,6 @@
 name:          bound
 category:      Language, Compilers/Interpreters
-version:       0.4
+version:       0.5
 license:       BSD3
 cabal-version: >= 1.9.2
 license-file:  LICENSE
@@ -21,6 +21,10 @@
    An untyped lambda calculus:
    .
    > import Bound
+   > import Control.Applicative
+   > import Control.Monad (ap)
+   > import Data.Foldable
+   > import Data.Traversable
    > import Prelude.Extras
    .
    > infixl 9 :@
@@ -98,7 +102,9 @@
   examples/Simple.hs
   examples/Deriving.hs
   examples/Overkill.hs
+  tests/doctests.hs
   README.markdown
+  CHANGELOG.markdown
 
 source-repository head
   type: git
@@ -106,27 +112,59 @@
 
 library
   hs-source-dirs: src
-  build-depends:
-    base           >= 4     && < 5,
-    bifunctors     >= 0.1.3 && < 0.2,
-    prelude-extras >= 0.2   && < 0.3,
-    transformers   >= 0.2   && < 0.4
 
   exposed-modules:
     Bound
     Bound.Class
+    Bound.Name
     Bound.Scope
     Bound.Term
     Bound.Var
 
-  ghc-options: -Wall -O2 -fspec-constr -fdicts-cheap
+  build-depends:
+    base           >= 4   && < 5,
+    bifunctors     == 3.0.*,
+    comonad        == 3.0.*,
+    prelude-extras >= 0.2 && < 0.3,
+    transformers   >= 0.2 && < 0.4
 
+  ghc-options: -Wall -O2 -fspec-constr -fdicts-cheap -funbox-strict-fields
+  if impl(ghc>=7.4)
+    build-depends: ghc-prim
+
+-- Stating these, despite being more correct, causes spurious warnings to
+-- end-users of older Cabal versions, so we don't.
+
+--  other-extensions: CPP
+--  if impl(ghc)
+--    other-extensions: DeriveDataTypeable
+--  if impl(ghc>=7.4)
+--    other-extensions: DeriveGeneric DefaultSignatures
+
 test-suite Simple
-  build-depends:
-    base           >= 4     && < 5,
-    prelude-extras >= 0.2   && < 0.3,
-    transformers   >= 0.2   && < 0.4,
-    bound
   type: exitcode-stdio-1.0
-  hs-source-dirs: examples
   main-is: Simple.hs
+  hs-source-dirs: examples
+  ghc-options -Wall -threaded
+  if impl(ghc<7.6.1)
+    ghc-options: -Werror
+  build-depends:
+    base,
+    bound,
+    prelude-extras,
+    transformers
+
+-- Verify the results of the examples
+test-suite doctests
+  type:    exitcode-stdio-1.0
+  main-is: doctests.hs
+  hs-source-dirs: tests
+  ghc-options: -Wall -threaded
+  if impl(ghc<7.6.1)
+    ghc-options: -Werror
+  build-depends:
+    base,
+    directory >= 1.0 && < 1.3,
+    doctest   >= 0.9 && < 0.10,
+    filepath,
+    vector    == 0.9.*
diff --git a/examples/Deriving.hs b/examples/Deriving.hs
--- a/examples/Deriving.hs
+++ b/examples/Deriving.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
-module Exp where
+module Deriving where
 
 import Data.List
 import Data.Foldable
@@ -61,6 +61,9 @@
 
 data P a = P { pattern :: [a] -> Pat Exp a, bindings :: [a] }
 
+-- |
+-- >>> lam (varp "x") (V "x")
+-- Lam 1 VarP (Scope (V (B 0)))
 varp :: a -> P a
 varp a = P (const VarP) [a]
 
@@ -70,6 +73,9 @@
 asp :: a -> P a -> P a
 asp a (P p as) = P (\bs -> AsP (p (a:bs))) (a:as)
 
+-- |
+-- >>> lam (conp "Hello" [varp "x", wildp]) (V "y")
+-- Lam 1 (ConP "Hello" [VarP,WildP]) (Scope (V (F (V "y"))))
 conp :: String -> [P a] -> P a
 conp g ps = P (ConP g . go ps) (ps >>= bindings)
   where
@@ -81,6 +87,15 @@
 viewp t (P p as) = P (\bs -> ViewP (abstract (`elemIndex` bs) t) (p bs)) as
 
 -- | smart lam constructor
+--
+-- >>> let_ [("x",V "y"),("y",V "x" :@ V "y")] $ lam (varp "z") (V "z" :@ V "y")
+-- Let 2 [Scope (V (B 1)),Scope (V (B 0) :@ V (B 1))] (Scope (Lam 1 VarP (Scope (V (B 0) :@ V (F (V (B 1)))))))
+--
+-- >>> lam (conp "F" [varp "x", viewp (V "x") $ varp "y"]) (V "y")
+-- Lam 2 (ConP "F" [VarP,ViewP (Scope (V (B 0))) VarP]) (Scope (V (B 1)))
+--
+-- >>> lam (conp "F" [varp "x", viewp (V "y") $ varp "y"]) (V "y")
+-- Lam 2 (ConP "F" [VarP,ViewP (Scope (V (F (V "y")))) VarP]) (Scope (V (B 1)))
 lam :: Eq a => P a -> Exp a -> Exp a
 lam (P p as) t = Lam (length as) (p []) (abstract (`elemIndex` as) t)
 
@@ -91,26 +106,11 @@
         abstr = abstract (`elemIndex` vs)
 
 -- | smart alt constructor
-alt :: Eq a => P a -> Exp a -> Alt Exp a
-alt (P p as) t = Alt (length as) (p []) (abstract (`elemIndex` as) t)
-
--- >>> let_ [("x",V "y"),("y",V "x" :@ V "y")] $ lam (varp "z") (V "z" :@ V "y")
--- Let 2 [Scope (V (B 1)),Scope (V (B 0) :@ V (B 1))] (Scope (Lam 1 VarP (Scope (V (B 0) :@ V (F (V (B 1)))))))
-
--- >>> lam (varp "x") (V "x")
--- Lam 1 VarP (Scope (V (B 0)))
-
--- >>> lam (conp "Hello" [varp "x", wildp]) (V "y")
--- Lam 1 (ConP "Hello" [VarP,WildP]) (Scope (V (F (V "y"))))
-
+--
 -- >>> lam (varp "x") $ Case (V "x") [alt (conp "Hello" [varp "z",wildp]) (V "x"), alt (varp "y") (V "y")]
 -- Lam 1 VarP (Scope (Case (V (B 0)) [Alt 1 (ConP "Hello" [VarP,WildP]) (Scope (V (F (V (B 0))))),Alt 1 VarP (Scope (V (B 0)))]))
-
--- view patterns can reference name from earlier in the same scope
--- >>> lam (conp "F" [varp "x", viewp (V "x") $ varp "y"]) (V "y")
--- Lam 2 (ConP "F" [VarP,ViewP (Scope (V (B 0))) VarP]) (Scope (V (B 1)))
-
--- but like in ghc, they refuse to allow references to subsequent bindings in the scope
--- >>> lam (conp "F" [varp "x", viewp (V "y") $ varp "y"]) (V "y")
--- Lam 2 (ConP "F" [VarP,ViewP (Scope (V (F (V "y")))) VarP]) (Scope (V (B 1)))
+alt :: Eq a => P a -> Exp a -> Alt Exp a
+alt (P p as) t = Alt (length as) (p []) (abstract (`elemIndex` as) t)
 
+main :: IO ()
+main = return ()
diff --git a/examples/Overkill.hs b/examples/Overkill.hs
--- a/examples/Overkill.hs
+++ b/examples/Overkill.hs
@@ -9,7 +9,7 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE TypeOperators #-}
-module Exp where
+module Overkill where
 
 import Data.Vector as Vector hiding ((++), map)
 import Data.List as List
@@ -189,8 +189,6 @@
   ViewP e p >>>= f = ViewP (e >>= f) (p >>>= f)
 
 -- ** Pats
-
-
 eqPats :: (Eq1 f, Eq a) => Pats bs f a -> Pats bs' f a -> Bool
 eqPats NilP      NilP      = True
 eqPats (p :> ps) (q :> qs) = eqPat p q && eqPats ps qs
@@ -221,9 +219,7 @@
   NilP >>>= _ = NilP
   (p :> ps) >>>= f = (p >>>= f) :> (ps >>>= f)
 
-
 -- ** Path into Pats
-
 eqMPath :: MPath is -> MPath js -> Bool
 eqMPath (H m) (H n) = eqPath m n
 eqMPath (T p) (T q) = eqMPath p q
@@ -244,8 +240,6 @@
 -- instance Read (MPath is)
 
 -- ** Path into Pat
-
-
 eqPath :: Path i -> Path j -> Bool
 eqPath V     V     = True
 eqPath L     L     = True
@@ -282,6 +276,14 @@
   showsPrec d (R m) = showParen (d > 10) $ showString "R " . showsPrec 11 m
   showsPrec d (C p) = showParen (d > 10) $ showString "C " . showsPrec 11 p
 
--- ghci> let_ [("x",Var "y"),("y",Var "x" :@ Var "y")] $ lam (varp "z") (Var "z" :@ Var "y")
--- ghci> lam (varp "x") (Var "x")
--- ghci> lam (conp "Hello" [varp "x", wildp])) (Var "y")
+-- |
+-- >>> let_ [("x",Var "y"),("y",Var "x" :@ Var "y")] $ lam (varp "z") (Var "z" :@ Var "y")
+-- Let (fromList [Scope (Var (B 1)),Scope (Var (B 0) :@ Var (B 1))]) (Scope (Lam VarP (Scope (Var (B V) :@ Var (F (Var (B 1)))))))
+--
+-- >>> lam (varp "x") (Var "x")
+-- Lam VarP (Scope (Var (B V)))
+--
+-- >>> lam (conp "Hello" [varp "x", wildp]) (Var "y")
+-- Lam (ConP "Hello" (VarP :> WildP :> NilP)) (Scope (Var (F (Var "y"))))
+main :: IO ()
+main = return ()
diff --git a/examples/Simple.hs b/examples/Simple.hs
--- a/examples/Simple.hs
+++ b/examples/Simple.hs
@@ -27,7 +27,7 @@
 -- | A smart constructor for Lam
 --
 -- >>> lam "y" (lam "x" (V "x" :@ V "y"))
--- Lam (Lam (V (B ()) :@ V (F (V (B ())))))
+-- Lam (Scope (Lam (Scope (V (B ()) :@ V (F (V (B ())))))))
 lam :: Eq a => a -> Exp a -> Exp a
 lam v b = Lam (abstract1 v b)
 
@@ -95,7 +95,7 @@
 --
 -- Modified to use recursive let, because we can.
 --
--- >>> nf cooked == lam "false" (lam "true" (V"false"))
+-- >>> nf cooked == true
 -- True
 
 true :: Exp String
diff --git a/src/Bound.hs b/src/Bound.hs
--- a/src/Bound.hs
+++ b/src/Bound.hs
@@ -9,44 +9,64 @@
 -- Portability :  portable
 --
 -- We represent the target language itself as an ideal monad supplied by the
--- user, and provide a 'Scope' monad transformer for introducing bound 
+-- user, and provide a 'Scope' monad transformer for introducing bound
 -- variables in user supplied terms. Users supply a 'Monad' and 'Traversable'
 -- instance, and we traverse to find free variables, and use the 'Monad' to
 -- perform substitution that avoids bound variables.
 --
 -- An untyped lambda calculus:
 --
--- > import Bound
--- > import Prelude.Extras
+-- @
+-- {-\# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable \#-}
+-- import Bound
+-- import Control.Applicative
+-- import Control.Monad ('Control.Monad.ap')
+-- import Prelude.Extras
+-- import Data.Foldable
+-- import Data.Traverable
+-- @
 --
--- > infixl 9 :@
--- > data Exp a = V a | Exp a :@ Exp a | Lam (Scope () Exp a)
--- >  deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)
+-- @
+-- infixl 9 :\@
+-- data Exp a = V a | Exp a :\@ Exp a | Lam ('Scope' () Exp a)
+--   deriving ('Eq','Ord','Show','Read','Functor','Data.Foldable.Foldable','Data.Foldable.Traversable')
+-- @
 --
--- > instance Eq1 Exp   where (==#)      = (==)
--- > instance Ord1 Exp  where compare1   = compare
--- > instance Show1 Exp where showsPrec1 = showsPrec
--- > instance Read1 Exp where readsPrec1 = readsPrec
--- > instance Applicative Exp where pure = V; (<*>) = ap
+-- @
+-- instance 'Prelude.Extras.Eq1' Exp   where ('Prelude.Extras.==#')      = ('==')
+-- instance 'Prelude.Extras.Ord1' Exp  where 'Prelude.Extras.compare1'   = 'compare'
+-- instance 'Prelude.Extras.Show1' Exp where 'Prelude.Extras.showsPrec1' = 'showsPrec'
+-- instance 'Prelude.Extras.Read1' Exp where 'Prelude.Extras.readsPrec1' = 'readsPrec'
+-- instance 'Control.Applicative.Applicative' Exp where 'Control.Applicative.pure' = V; ('<*>') = 'Control.Monad.ap'
+-- @
 --
--- > 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)
+-- @
+-- instance 'Monad' Exp where
+--   'return' = V
+--   V a      '>>=' f = f a
+--   (x :\@ y) '>>=' f = (x '>>=' f) :\@ (y >>= f)
+--   Lam e    '>>=' f = Lam (e '>>>=' f)
+-- @
 --
--- > whnf :: Exp a -> Exp a
--- > whnf (f :@ a) = case whnf f of
--- >   Lam b -> whnf (instantiate1 a b)
--- >   f'    -> f' :@ a
--- > whnf e = e
+-- @
+-- lam :: 'Eq' a => a -> 'Exp' a -> 'Exp' a
+-- lam v b = Lam ('abstract1' v b)
+-- @
 --
+-- @
+-- whnf :: 'Exp' a -> 'Exp' a
+-- whnf (f :\@ a) = case whnf f of
+--   Lam b -> whnf ('instantiate1' a b)
+--   f'    -> f' :\@ a
+-- whnf e = e
+-- @
+--
 -- More exotic combinators for manipulating a 'Scope' can be imported from
 -- "Bound.Scope".
 --
+-- You can also retain names in your bound variables by using 'Bound.Name.Name'
+-- and the related combinators from "Bound.Name". They are not re-exported
+-- from this module by default.
 ----------------------------------------------------------------------------
 module Bound
   (
diff --git a/src/Bound/Class.hs b/src/Bound/Class.hs
--- a/src/Bound/Class.hs
+++ b/src/Bound/Class.hs
@@ -12,6 +12,8 @@
 -- Stability   :  experimental
 -- Portability :  portable
 --
+-- This module provides the 'Bound' class, for performing substitution into
+-- things that are not necessarily full monad transformers.
 ----------------------------------------------------------------------------
 module Bound.Class
   ( Bound(..)
@@ -24,15 +26,22 @@
 
 infixl 1 >>>=
 
--- | Instances may or may not be monad transformers.
+-- | Instances of 'Bound' may or may not be monad transformers.
 --
--- If they are, then you can use @m >>>= f = m >>= lift . f@
+-- If they are, then @m '>>>=' f ≡ m '>>=' 'lift' '.' f@ is required to hold, and is
+-- in fact the default definition. If it is not a 'MonadTrans' instance, then
+-- you have greater flexibility in how to implement this class.
 --
 -- This is useful for types like expression lists, case alternatives,
 -- schemas, etc. that may not be expressions in their own right, but often
--- contain one.
-
+-- contain expressions.
 class Bound t where
+  -- | Perform substitution
+  --
+  -- If @t@ is an instance of @MonadTrans@ and you are compiling on GHC >= 7.4, then this
+  -- gets the default definition:
+  --
+  -- @m '>>>=' f = m '>>=' 'lift' '.' f@
   (>>>=) :: Monad f => t f a -> (a -> f c) -> t f c
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 704
   default (>>>=) :: (MonadTrans t, Monad f, Monad (t f)) =>
@@ -41,5 +50,8 @@
 #endif
 
 infixr 1 =<<<
+-- | A flipped version of ('>>>=').
+--
+-- @('=<<<') = 'flip' ('>>>=')@
 (=<<<) :: (Bound t, Monad f) => (a -> f c) -> t f a -> t f c
 (=<<<) = flip (>>>=)
diff --git a/src/Bound/Name.hs b/src/Bound/Name.hs
new file mode 100644
--- /dev/null
+++ b/src/Bound/Name.hs
@@ -0,0 +1,162 @@
+{-# LANGUAGE CPP #-}
+#ifdef __GLASGOW_HASKELL__
+{-# LANGUAGE DeriveDataTypeable #-}
+
+# if __GLASGOW_HASKELL__ >= 704
+{-# LANGUAGE DeriveGeneric #-}
+# endif
+
+#endif
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Bound.Name
+-- Copyright   :  (C) 2012 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  experimental
+-- Portability :  portable
+--
+-- The problem with locally nameless approaches is that original names are
+-- often useful for error reporting, or to allow for the user in an interactive
+-- theorem prover to convey some hint about the domain. A @'Name' n b@ is a value
+-- @b@ supplemented with a (discardable) name that may be useful for error
+-- reporting purposes. In particular, this name does not participate in
+-- comparisons for equality.
+--
+-- This module is /not/ exported from "Bound" by default. You need to explicitly
+-- import it, due to the fact that 'Name' is a pretty common term in other
+-- people's code.
+----------------------------------------------------------------------------
+module Bound.Name
+  ( Name(..)
+  , name
+  , abstractName
+  , abstract1Name
+  , instantiateName
+  , instantiate1Name
+  ) where
+
+import Bound.Scope
+import Bound.Var
+import Data.Foldable
+import Data.Traversable
+import Data.Monoid
+import Data.Bifunctor
+import Data.Bifoldable
+import Data.Bitraversable
+#ifdef __GLASGOW_HASKELL__
+import Data.Data
+# if __GLASGOW_HASKELL__ >= 704
+import GHC.Generics
+# endif
+#endif
+import Control.Applicative
+import Control.Comonad
+import Control.Monad (liftM)
+import Prelude.Extras
+
+-------------------------------------------------------------------------------
+-- Names
+-------------------------------------------------------------------------------
+
+-- |
+-- We track the choice of 'Name' @n@ as a forgettable property that does /not/ affect
+-- the result of ('==') or 'compare'.
+--
+-- To compare names rather than values, use @('Data.Function.on' 'compare' 'name')@ instead.
+data Name n b = Name n b deriving
+  ( Show
+  , Read
+#ifdef __GLASGOW_HASKELL__
+  , Typeable
+  , Data
+# if __GLASGOW_HASKELL__ >= 704
+  , Generic
+# endif
+#endif
+  )
+
+-- | Extract the 'name'.
+name :: Name n b -> n
+name (Name n _) = n
+
+-------------------------------------------------------------------------------
+-- Instances
+-------------------------------------------------------------------------------
+
+instance Eq b => Eq (Name n b) where
+  Name _ a == Name _ b = a == b
+
+instance Ord b => Ord (Name n b) where
+  Name _ a `compare` Name _ b = compare a b
+
+instance Functor (Name n) where
+  fmap f (Name n a) = Name n (f a)
+
+instance Foldable (Name n) where
+  foldMap f (Name _ a) = f a
+
+instance Traversable (Name n) where
+  traverse f (Name n a) = Name n <$> f a
+
+instance Bifunctor Name where
+  bimap f g (Name n a) = Name (f n) (g a)
+
+instance Bifoldable Name where
+  bifoldMap f g (Name n a) = f n `mappend` g a
+
+instance Bitraversable Name where
+  bitraverse f g (Name n a) = Name <$> f n <*> g a
+
+instance Comonad (Name n) where
+  extract (Name _ b) = b
+  extend f w@(Name n _) = Name n (f w)
+
+instance Eq1   (Name b) where (==#)      = (==)
+instance Ord1  (Name b) where compare1   = compare
+instance Show b => Show1 (Name b) where showsPrec1 = showsPrec
+instance Read b => Read1 (Name b) where readsPrec1 = readsPrec
+
+-- these are slightly too restrictive, but still safe
+instance Eq2 Name   where (==##)     = (==)
+instance Ord2 Name  where compare2   = compare
+instance Show2 Name where showsPrec2 = showsPrec
+instance Read2 Name where readsPrec2  = readsPrec
+
+-------------------------------------------------------------------------------
+-- Abstraction
+-------------------------------------------------------------------------------
+
+-- | Abstraction, capturing named bound variables.
+abstractName :: Monad f => (a -> Maybe b) -> f a -> Scope (Name a b) f a
+abstractName f t = Scope (liftM k t) where
+  k a = case f a of
+    Just b  -> B (Name a b)
+    Nothing -> F (return a)
+{-# INLINE abstractName #-}
+
+-- | Abstract over a single variable
+abstract1Name :: (Monad f, Eq a) => a -> f a -> Scope (Name a ()) f a
+abstract1Name a = abstractName (\b -> if a == b then Just () else Nothing)
+{-# INLINE abstract1Name #-}
+
+-------------------------------------------------------------------------------
+-- Instantiation
+-------------------------------------------------------------------------------
+
+-- | Enter a scope, instantiating all bound variables, but discarding (comonadic)
+-- meta data, like its name
+instantiateName :: (Monad f, Comonad n) => (b -> f a) -> Scope (n b) f a -> f a
+instantiateName k e = unscope e >>= \v -> case v of
+  B b -> k (extract b)
+  F a -> a
+{-# INLINE instantiateName #-}
+
+
+-- | Enter a 'Scope' that binds one (named) variable, instantiating it.
+--
+-- @'instantiate1Name' = 'instantiate1'@
+instantiate1Name :: Monad f => f a -> Scope n f a -> f a
+instantiate1Name = instantiate1
+{-# INLINE instantiate1Name #-}
diff --git a/src/Bound/Scope.hs b/src/Bound/Scope.hs
--- a/src/Bound/Scope.hs
+++ b/src/Bound/Scope.hs
@@ -8,6 +8,10 @@
 -- Stability   :  experimental
 -- Portability :  portable
 --
+-- This is the work-horse of the @bound@ library.
+--
+-- 'Scope' provides a single generalized de Bruijn level
+-- and is often used inside of the definition of binders.
 ----------------------------------------------------------------------------
 module Bound.Scope
   ( Scope(..)
@@ -51,6 +55,10 @@
 import Prelude.Extras
 import Prelude hiding (foldr, mapM, mapM_)
 
+-------------------------------------------------------------------------------
+-- Scopes
+-------------------------------------------------------------------------------
+
 -- | @'Scope' b f a@ is an @f@ expression with bound variables in @b@,
 -- and free variables in @a@
 --
@@ -72,6 +80,10 @@
 --
 newtype Scope b f a = Scope { unscope :: f (Var b (f a)) }
 
+-------------------------------------------------------------------------------
+-- Instances
+-------------------------------------------------------------------------------
+
 instance Functor f => Functor (Scope b f) where
   fmap f (Scope a) = Scope (fmap (fmap (fmap f)) a)
 
@@ -122,8 +134,16 @@
 instance Bound (Scope b) where
   Scope m >>>= f = Scope (liftM (fmap (>>= f)) m)
 
+-------------------------------------------------------------------------------
+-- Abstraction
+-------------------------------------------------------------------------------
+
 -- | Capture some free variables in an expression to yield
 -- a 'Scope' with bound variables in @b@
+--
+-- >>> :m + Data.List
+-- >>> abstract (`elemIndex` "bar") "barry"
+-- Scope [B 0,B 1,B 2,B 2,F "y"]
 abstract :: Monad f => (a -> Maybe b) -> f a -> Scope b f a
 abstract f e = Scope (liftM k e) where
   k y = case f y of
@@ -131,33 +151,54 @@
     Nothing -> F (return y)
 {-# INLINE abstract #-}
 
+-- | Abstract over a single variable
+--
+-- >>> abstract1 'x' "xyz"
+-- Scope [B (),F "y",F "z"]
+abstract1 :: (Monad f, Eq a) => a -> f a -> Scope () f a
+abstract1 a = abstract (\b -> if a == b then Just () else Nothing)
+{-# INLINE abstract1 #-}
+
+-------------------------------------------------------------------------------
+-- Instantiation
+-------------------------------------------------------------------------------
+
 -- | Enter a scope, instantiating all bound variables
+--
+-- >>> :m + Data.List
+-- >>> instantiate (\x -> [toEnum (97 + x)]) $ abstract (`elemIndex` "bar") "barry"
+-- "abccy"
 instantiate :: Monad f => (b -> f a) -> Scope b f a -> f a
 instantiate k e = unscope e >>= \v -> case v of
   B b -> k b
   F a -> a
 {-# INLINE instantiate #-}
 
--- * Special purpose combinators
-
--- | Abstract over a single variable
-abstract1 :: (Monad f, Eq a) => a -> f a -> Scope () f a
-abstract1 a = abstract (\b -> if a == b then Just () else Nothing)
-{-# INLINE abstract1 #-}
-
 -- | Enter a 'Scope' that binds one variable, instantiating it
-instantiate1 :: Monad f => f a -> Scope () f a -> f a
+--
+-- >>> instantiate1 "x" $ Scope [B (),F "y",F "z"]
+-- "xyz"
+instantiate1 :: Monad f => f a -> Scope n f a -> f a
 instantiate1 e = instantiate (const e)
 {-# INLINE instantiate1 #-}
 
+-------------------------------------------------------------------------------
+-- Traditional de Bruijn
+-------------------------------------------------------------------------------
+
 -- | @'fromScope'@ quotients out the possible placements of 'F' in 'Scope'
 -- by distributing them all to the leaves. This yields a more traditional
 -- de Bruijn indexing scheme for bound variables.
 --
--- > fromScope . toScope = id
--- > fromScope . toScope . fromScope = fromScope
+-- Since,
 --
--- @('toScope' . 'fromScope')@ is idempotent
+-- @'fromScope' '.' 'toScope' ≡ 'id'@
+--
+-- we know that
+--
+-- @'fromScope' '.' 'toScope' '.' 'fromScope' ≡ 'fromScope'@
+--
+-- and therefore @('toScope' . 'fromScope')@ is idempotent.
 fromScope :: Monad f => Scope b f a -> f (Var b a)
 fromScope (Scope s) = s >>= \v -> case v of
   F e -> liftM F e
@@ -171,21 +212,25 @@
 toScope e = Scope (liftM (fmap return) e)
 {-# INLINE toScope #-}
 
--- | Perform substitution on both bound and free variables in a 'Scope'
+-------------------------------------------------------------------------------
+-- Exotic Traversals of Bound Variables (not exported by default)
+-------------------------------------------------------------------------------
+
+-- | Perform substitution on both bound and free variables in a 'Scope'.
 splat :: Monad f => (a -> f c) -> (b -> f c) -> Scope b f a -> f c
 splat f unbind s = unscope s >>= \v -> case v of
   B b -> unbind b
   F ea -> ea >>= f
 {-# INLINE splat #-}
 
--- Return a list of occurences of the variables bound by this scope
+-- | Return a list of occurences of the variables bound by this 'Scope'.
 bindings :: Foldable f => Scope b f a -> [b]
 bindings (Scope s) = foldr f [] s where
   f (B v) vs = v : vs
   f _ vs     = vs
 {-# INLINE bindings #-}
 
--- | Perform a change of variables on bound variables
+-- | Perform a change of variables on bound variables.
 mapBound :: Functor f => (b -> b') -> Scope b f a -> Scope b' f a
 mapBound f (Scope s) = Scope (fmap f' s) where
   f' (B b) = B (f b)
@@ -226,6 +271,7 @@
 foldMapScope f g (Scope s) = foldMap (bifoldMap f (foldMap g)) s
 {-# INLINE foldMapScope #-}
 
+-- | 'traverse_' the bound variables in a 'Scope'.
 traverseBound_ :: (Applicative g, Foldable f) =>
                   (b -> g d) -> Scope b f a -> g ()
 traverseBound_ f (Scope s) = traverse_ f' s
@@ -233,7 +279,7 @@
         f' _     = pure ()
 {-# INLINE traverseBound_ #-}
 
---- | Traverse both the variables bound by this scope and any free variables.
+-- | 'traverse' both the variables bound by this scope and any free variables.
 traverseScope_ :: (Applicative g, Foldable f) =>
                   (b -> g d) -> (a -> g c) -> Scope b f a -> g ()
 traverseScope_ f g (Scope s) = traverse_ (bitraverse_ f (traverse_ g)) s
@@ -253,7 +299,7 @@
 mapMScope_ f g (Scope s) = mapM_ (bimapM_ f (mapM_ g)) s
 {-# INLINE mapMScope_ #-}
 
---- | Traverse both bound and free variables
+-- | Traverse both bound and free variables
 traverseBound :: (Applicative g, Traversable f) =>
                  (b -> g c) -> Scope b f a -> g (Scope c f a)
 traverseBound f (Scope s) = Scope <$> traverse f' s where
@@ -261,13 +307,13 @@
   f' (F a) = pure (F a)
 {-# INLINE traverseBound #-}
 
---- | Traverse both bound and free variables
+-- | Traverse both bound and free variables
 traverseScope :: (Applicative g, Traversable f) =>
                  (b -> g d) -> (a -> g c) -> Scope b f a -> g (Scope d f c)
 traverseScope f g (Scope s) = Scope <$> traverse (bitraverse f (traverse g)) s
 {-# INLINE traverseScope #-}
 
---- | mapM over both bound and free variables
+-- | mapM over both bound and free variables
 mapMBound :: (Monad m, Traversable f) =>
              (b -> m c) -> Scope b f a -> m (Scope c f a)
 mapMBound f (Scope s) = liftM Scope (mapM f' s) where
@@ -275,7 +321,7 @@
   f' (F a) = return (F a)
 {-# INLINE mapMBound #-}
 
---- | A 'traverseScope' that can be used when you only have a 'Monad'
+-- | A 'traverseScope' that can be used when you only have a 'Monad'
 -- instance
 mapMScope :: (Monad m, Traversable f) =>
              (b -> m d) -> (a -> m c) -> Scope b f a -> m (Scope d f c)
diff --git a/src/Bound/Term.hs b/src/Bound/Term.hs
--- a/src/Bound/Term.hs
+++ b/src/Bound/Term.hs
@@ -11,6 +11,7 @@
 ----------------------------------------------------------------------------
 module Bound.Term
   ( substitute
+  , substituteVar
   , isClosed
   , closed
   ) where
@@ -19,18 +20,44 @@
 import Data.Traversable
 import Prelude hiding (all)
 
--- | @'substitute' a p w@ replaces the free variable @a@ with @p@ in @w@
+-- | @'substitute' a p w@ replaces the free variable @a@ with @p@ in @w@.
+--
+-- >>> substitute "hello" ["goodnight","Gracie"] ["hello","!!!"]
+-- ["goodnight","Gracie","!!!"]
 substitute :: (Monad f, Eq a) => a -> f a -> f a -> f a
 substitute a p w = w >>= \b -> if a == b then p else return b
 {-# INLINE substitute #-}
 
+-- | @'substituteVar' a b w@ replaces a free variable @a@ with another free variable @b@ in @w@.
+--
+-- >>> substituteVar "Alice" "Bob" ["Alice","Bob","Charlie"]
+-- ["Bob","Bob","Charlie"]
+substituteVar :: (Functor f, Eq a) => a -> a -> f a -> f a
+substituteVar a p = fmap (\b -> if a == b then p else b)
+{-# INLINE substituteVar #-}
+
 -- | If a term has no free variables, you can freely change the type of
 -- free variables it is parameterized on.
+--
+-- >>> closed [12]
+-- Nothing
+--
+-- >>> closed ""
+-- Just []
+--
+-- >>> :t closed ""
+-- closed "" :: Maybe [b]
 closed :: Traversable f => f a -> Maybe (f b)
 closed = traverse (const Nothing)
 {-# INLINE closed #-}
 
 -- | A closed term has no free variables.
+--
+-- >>> isClosed []
+-- True
+--
+-- >>> isClosed [1,2,3]
+-- False
 isClosed :: Foldable f => f a -> Bool
 isClosed = all (const False)
 {-# INLINE isClosed #-}
diff --git a/src/Bound/Var.hs b/src/Bound/Var.hs
--- a/src/Bound/Var.hs
+++ b/src/Bound/Var.hs
@@ -1,3 +1,13 @@
+{-# LANGUAGE CPP #-}
+
+#ifdef __GLASGOW_HASKELL__
+{-# LANGUAGE DeriveDataTypeable #-}
+
+# if __GLASGOW_HASKELL__ >= 704
+{-# LANGUAGE DeriveGeneric #-}
+# endif
+
+#endif
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Bound.Var
@@ -13,26 +23,52 @@
   ( Var(..)
   ) where
 
+import Control.Applicative
+import Control.Monad (ap)
 import Data.Foldable
 import Data.Traversable
 import Data.Monoid (mempty)
 import Data.Bifunctor
 import Data.Bifoldable
 import Data.Bitraversable
-import Control.Applicative
-import Control.Monad (ap)
+#ifdef __GLASGOW_HASKELL__
+import Data.Data
+# if __GLASGOW_HASKELL__ >= 704
+import GHC.Generics
+# endif
+#endif
 import Prelude.Extras
 
+----------------------------------------------------------------------------
+-- Bound and Free Variables
+----------------------------------------------------------------------------
+
 -- | \"I am not a number, I am a /free monad/!\"
 --
--- A @Var b a@ is a variable that may either be \"bound\" or \"free\".
+-- A @'Var' b a@ is a variable that may either be \"bound\" ('B') or \"free\" ('F').
 --
--- (It is also technically a free monad in the same near trivial sense as
+-- (It is also technically a free monad in the same near-trivial sense as
 -- 'Either'.)
 data Var b a
   = B b -- ^ this is a bound variable
   | F a -- ^ this is a free variable
-  deriving (Eq,Ord,Show,Read)
+  deriving
+  ( Eq
+  , Ord
+  , Show
+  , Read
+#ifdef __GLASGOW_HASKELL__
+  , Data
+  , Typeable
+# if __GLASGOW_HASKELL__ >= 704
+  , Generic
+# endif
+#endif
+  )
+
+----------------------------------------------------------------------------
+-- Instances
+----------------------------------------------------------------------------
 
 instance Functor (Var b) where
   fmap _ (B b) = B b
diff --git a/tests/doctests.hs b/tests/doctests.hs
new file mode 100644
--- /dev/null
+++ b/tests/doctests.hs
@@ -0,0 +1,32 @@
+module Main where
+
+import Test.DocTest
+import System.Directory
+import System.FilePath
+import Control.Applicative
+import Control.Monad
+import Data.List
+
+main :: IO ()
+main = getSources >>= \sources -> doctest $
+    "-iexamples"
+  : "-isrc"
+  : "-idist/build/autogen"
+  : "-optP-include"
+  : "-optPdist/build/autogen/cabal_macros.h"
+  : sources
+
+getSources :: IO [FilePath]
+getSources = do
+  examples <- go "examples"
+  src <- go "src"
+  return $ filter (isSuffixOf ".hs") (examples ++ src)
+  where
+    go dir = do
+      (dirs, files) <- getFilesAndDirectories dir
+      (files ++) . concat <$> mapM go dirs
+
+getFilesAndDirectories :: FilePath -> IO ([FilePath], [FilePath])
+getFilesAndDirectories dir = do
+  c <- map (dir </>) . filter (`notElem` ["..", "."]) <$> getDirectoryContents dir
+  (,) <$> filterM doesDirectoryExist c <*> filterM doesFileExist c