diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,13 @@
 # Revision history for property-matchers
 
+## 0.5
+* Add `notEquals` property.
+* Delete `atIndex`, `endingWith`, and `startingWith`. These can easily be replaced by prisms via `match`, like with `match (ix k)`, `match _head`, and `match _last`.
+* Delete `bool` in favor of `equals True`.
+* Export `Getting` in case it's useful.
+* Add some doctests.
+* Update docs.
+
 ## 0.4
 * Fix `allOf1` which would fail on a non-empty input, instead of the opposite
 * Add `anyOf`
diff --git a/property-matchers.cabal b/property-matchers.cabal
--- a/property-matchers.cabal
+++ b/property-matchers.cabal
@@ -1,7 +1,7 @@
 cabal-version: 2.4
 
 name: property-matchers
-version: 0.4.0.0
+version: 0.5.0.0
 synopsis: A library for tests, based on transforming and writing properties
 description:
   This package provides ways to write properties for testing such that they compose nicely and are easy to debug.
diff --git a/src/PropertyMatchers.hs b/src/PropertyMatchers.hs
--- a/src/PropertyMatchers.hs
+++ b/src/PropertyMatchers.hs
@@ -14,16 +14,17 @@
 {-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE TypeApplications #-}
 
--- | This library is based on the notion of a property transformer, the below
--- type @PT a b@, which is a function from @a@ to properties on @b@.
--- They act as a sort of compositional "matcher language".
--- Composing these property transformers is meant to be analogous to composing optics
--- and there are utilities for using property transformers with (lens-style) optics.
---
--- Some property transformers provided by other libraries:
--- `Data.Foldable.all`, `Data.Foldable.any` (base)
--- `either` (base)
--- `Control.Lens.allOf` (lens)
+-- | This library is based on the notion of a property, a function `a -> IO ()`,
+-- which can be transformed and composed. They act as a sort of compositional
+-- "matcher language". Composing these property transformers is meant to be
+-- analogous to composing optics and there are utilities for using property
+-- transformers with (lens-style) optics.
+
+-- Designed for qualified import except for operators.
+
+-- >>> import PropertyMatchers qualified as P
+-- >>> import PropertyMatchers (pattern (:=>), (?))
+
 module PropertyMatchers
   ( Assertion
   , Boolish(..)
@@ -33,10 +34,8 @@
   , PropertyException(..)
   , Prop
   , PT
-  , endingWith
-  , startingWith
+  , Getting
   , match
-  , atIndex
   , list
   , alignExact
   , alignLax
@@ -47,18 +46,18 @@
   , allOf1
   , pair
   , fun
-  , fails
+  , throws
   , traced
   , tracedShow
   , traceFailShow
   , traceFail
   , forced
   , equals
+  , notEquals
   , lt
   , lte
   , gt
   , gte
-  , bool
   , pattern (:=>)
   , (?)
   )
@@ -67,8 +66,8 @@
 import Prelude hiding (and, elem, fail, or)
 import Control.Concurrent (myThreadId)
 import Control.Exception
+import Control.Monad (void)
 import qualified Data.Align as Align
-import Data.Foldable (toList)
 import Data.Functor.Const
 import Data.These
 import Data.Typeable
@@ -85,9 +84,35 @@
 import "recover-rtti" Debug.RecoverRTTI (anythingToString)
 import Data.IORef
 
+-- $setup
+-- >>> :set -XOverloadedStrings -XTypeApplications
+-- >>> import Control.Lens
+-- >>> import Data.Function ((&))
+-- >>> import Data.Bool (bool)
+-- >>> import qualified Data.List as List
+-- >>> import System.IO.Unsafe (unsafePerformIO)
+-- >>> :{
+--   failureMessage x
+--       = try @PropertyException x
+--       & unsafePerformIO
+--       & over _Left prettyExnWithoutCallStack
+-- :}
+--
+-- >>> :{
+--   contains message exnMsg = bool
+--     (fail ("message starting with " <> PP.pretty message))
+--     succeed
+--     (message `List.isInfixOf` exnMsg)
+--     exnMsg
+-- :}
+--
+
+-- | Returned by all properties.
+-- Enables applying properties using `>>=` and `Data.Function.&`, for example, in a do-block.
 type Assertion = IO ()
 
 -- | Internal, mostly the same as `catch` in safe-exceptions.
+--
 trySync :: Exception e => IO a -> IO (Either e a)
 trySync act = catches (Right <$> act)
   -- explicitly do not handle async exceptions.
@@ -95,8 +120,7 @@
   [ Handler $ \(ex :: SomeAsyncException) -> do
     tid <- myThreadId
     throwTo tid ex
-    -- unreachable
-    return undefined
+    evaluate (error "unreachable")
   , Handler $ \(ex :: e) ->
     return $ Left ex
   ]
@@ -116,47 +140,68 @@
 
 -- | The exception thrown by properties of type `Assertion` by default.
 -- Other non-async exceptions will work fine too.
+--
 data PropertyException
   = forall actual ann. PropertyFailed !CallStack (PP.Doc ann) actual
   | forall actual. NoBranchMatched !CallStack actual
   deriving (Typeable)
-instance Show PropertyException where
-  show = displayException
+instance PP.Pretty PropertyException where
+  pretty exn@(PropertyFailed cs _expected _actual) =
+    prettyExnWithoutCallStack exn
+    <> PP.hardline <> PP.pretty (prettyCallStack cs)
+  pretty exn@(NoBranchMatched cs _actual) =
+    prettyExnWithoutCallStack exn
+    <> PP.hardline <> PP.pretty (prettyCallStack cs)
 
+-- | Internal. Used for doctests.
+prettyExnWithoutCallStack :: PropertyException -> PP.Doc ann
+prettyExnWithoutCallStack (PropertyFailed _cs expected actual) =
+  PP.group
+    ( PP.line'
+    <> PP.flatAlt "Actual:" "Actual value"
+    <> PP.softline <> PP.pretty prettyActual
+    <> PP.line' <> PP.line
+    <> PP.flatAlt "Expected:" "but expected"
+    <> PP.softline <> PP.unAnnotate expected
+    )
+  where
+  prettyActual = anythingToTextPretty actual
+prettyExnWithoutCallStack (NoBranchMatched _cs actual) =
+  PP.group
+    ( PP.line'
+    <> PP.flatAlt "Actual:" "Actual value"
+    <> PP.softline <> PP.pretty prettyActual
+    <> PP.line' <> PP.line
+    <> "did not match any branches"
+    )
+  where
+  prettyActual = anythingToTextPretty actual
+
 instance Exception PropertyException where
-  displayException (PropertyFailed cs expected actual) =
-    PP.renderString $ PP.layoutSmart PP.defaultLayoutOptions $
-      PP.group
-        ( PP.line'
-        <> PP.flatAlt "Actual:" "Actual value"
-        <> PP.softline <> PP.pretty prettyActual
-        <> PP.line' <> PP.line
-        <> PP.flatAlt "Expected:" "but expected"
-        <> PP.softline <> expected
-        )
-      <> PP.hardline <> PP.pretty (prettyCallStack cs)
-    where
-    prettyActual = anythingToTextPretty actual
-  displayException (NoBranchMatched cs actual) =
-    PP.renderString $ PP.layoutSmart PP.defaultLayoutOptions $
-      PP.group
-        ( PP.line'
-        <> PP.flatAlt "Actual:" "Actual value"
-        <> PP.softline <> PP.pretty prettyActual
-        <> PP.line' <> PP.line
-        <> "did not match any branches"
-        )
-      <> PP.hardline <> PP.pretty (prettyCallStack cs)
-    where
-    prettyActual = anythingToTextPretty actual
+  displayException =
+    PP.renderString . PP.layoutSmart PP.defaultLayoutOptions . PP.pretty
 
--- | Successful assertion. Includes documentation of the failed expectation,
+instance Show PropertyException where
+  show = displayException
+
+-- | Failed property. Includes documentation of the failed property,
 -- as well as the asserted-on value for printing to the user.
--- Doubles as an always-failing property,
-fail :: HasCallStack => PP.Doc ann -> Prop a
+--
+-- >>> let actual = 42
+-- >>> :{
+--   actual
+--     & fail (PP.pretty "something else")
+--     & failureMessage
+-- :}
+-- Left Actual value 42 but expected something else
+fail :: HasCallStack => PP.Doc ann -> a -> IO x
 fail expected actual = throwIO (PropertyFailed (popCallStack callStack) expected actual)
 
--- | Always-successful property, equivalent to `\_ -> pure ()`.
+-- | Always-successful property, equivalent to @\_ -> pure ()@.
+--
+-- >>> let actual = 42
+-- >>> succeed actual
+--
 succeed :: actual -> Assertion
 succeed _ = pure ()
 {-# INLINE CONLIKE succeed #-}
@@ -165,6 +210,7 @@
 -- `or` and `and` should each be associative, idempotent, more or less
 -- commutative (because there may be multiple falsy values) and distribute
 -- over one another.
+--
 class Boolish p where
   or :: p -> p -> p
   and :: p -> p -> p
@@ -193,6 +239,7 @@
 
 -- | Non-backtracking branching. Use this to improve error messages and
 -- performance by avoiding testing properties that can never succeed.
+--
 branch :: (HasCallStack, Foldable t) => t (PT a b, Prop a) -> Prop b
 branch bs actual = foldr
     (\(cond, alt) fallback -> do
@@ -216,31 +263,21 @@
 {-# INLINABLE branch #-}
 
 -- | A convenient alias for properties.
+--
 type Prop a = a -> Assertion
 
 -- | Property transformers form a category where composition is ordinary function composition.
---  Forms a category with `.` and `id`.
---  Multiple are already provided by the standard library,
---  for instance `Data.Foldable.all` and `Data.Foldable.any`.
+-- Forms a category with `.` and `id`.
+--
 type PT a b = Prop a -> Prop b
 
--- | Operate on the last value in a foldable, or fail if it's not present.
-endingWith :: (HasCallStack, Foldable f) => PT a (f a)
-endingWith _ actual@(toList -> []) = fail "nonempty foldable" actual
-endingWith p (toList -> xs) = p $ last xs
-{-# INLINABLE endingWith #-}
-
--- | Operate on the first value in a foldable, or fail if it's not present.
-startingWith :: (HasCallStack, Foldable f) => PT a (f a)
-startingWith _ actual@(toList -> []) = fail "nonempty foldable" actual
-startingWith p (toList -> (x : _)) = p x
-{-# INLINABLE startingWith #-}
-
--- | Internal, just for `match`.
+-- | Ported from `lens` just for `match`.
+--
 type Getting r s a = (a -> Const r a) -> s -> Const r s
 
 -- | Require that a @Prism@ or any other @Fold@ matches, and apply the property
 -- to its target, only succeeding if there's exactly one target.
+--
 match
   :: (HasCallStack)
   => Getting [a] s a
@@ -250,13 +287,19 @@
     Const [x] -> p x
     _ -> fail "fold to match" s
 
--- | Test the element of a foldable at some index.
-atIndex :: (Foldable f) => Int -> PT a (f a)
-atIndex k p = startingWith p . drop k . toList
-
 -- | Given a list of properties and a list of values, ensure that each property
 -- holds for each respective value. Fails if the two lists have different
 -- lengths.
+--
+-- >>> [1, 2, 3] & list [equals 1, equals 2, equals 3]
+-- >>> -- succeeds
+-- >>> :{
+--   [1]
+--     & list [equals 1, equals 2, equals 3]
+--     & failureMessage
+-- :}
+-- Left Actual value [ 1 ] but expected list with length 3
+--
 list :: (HasCallStack) => [Prop a] -> [a] -> Assertion
 list ps xs
   | psl == length xs = foldr and (succeed xs) (zipWith ($) ps xs)
@@ -267,7 +310,17 @@
 -- | Given a functor-full of properties, and a functor-full of values, align
 -- the two together and apply all of the properties to the values pointwise.
 -- If there is any misalignment between the two, fail.
--- Generalized version of `list`.
+--
+-- Generalized version of `list`:
+--
+-- > list = alignExact
+--
+-- Example:
+--
+-- > P.alignExact (Map.singleton "a" (P.equals 2)) (Map.singleton "2" 2) -- success
+-- > P.alignExact Map.empty (Map.singleton "2" 2) -- failure
+-- > P.alignExact (Map.singleton "a" (P.equals 2)) Map.empty -- failure
+--
 alignExact
   :: (HasCallStack, Traversable f, Align.Semialign f) =>
   f (Prop a) ->
@@ -275,19 +328,30 @@
 alignExact props values =
   sequence_ $ Align.alignWith
     (\case
-      This _extraProp -> fail ("no extra elements relative to " <> PP.pretty (anythingToTextPretty props)) values
-      That _extraValue -> fail ("no missing elements relative to " <> PP.pretty (anythingToTextPretty props)) values
+      This _extraProp -> fail ("no extra elements relative to " <> PP.pretty (anythingToTextPretty $ void props)) values
+      That _extraValue -> fail ("no missing elements relative to " <> PP.pretty (anythingToTextPretty $ void props)) values
       These prop value -> prop value
       )
     props values
 
 -- | Given a functor-full of properties and a functor-full of values
 -- (and a property for excess values) align the properties and values and apply
--- them to each other pointwise. If there is any misalignment between the two:
---   * if there's an excess value, apply the excess property to it
---   * if there's a missing value, pass the corresponding property `Nothing`
+-- the props to the values pointwise. If there is any misalignment between the two:
+--
+--   - if there's a value with no corresponding prop, apply the excess property to it
+--   - if there's a prop with no corresponding value, pass the property `Nothing`
+--
+-- Generalized version of `alignExact`:
+--
+-- > alignExact props values =
+-- >  alignLax (P.fail "no extra elements") (P.match _Just <$> props) values
+--
 -- Examples:
--- alignLax (Map.fromList ["k" :=> P.lt 3, "g" :=> P.match P.gt 4]) (Map.fromList )
+--
+-- > P.alignLax
+-- >   (P.lt 5)
+-- >   (Map.fromList ["k" :=> P.match _Just ? P.lt 3, "g" :=> P.match _Just ? P.gt 4])
+-- >   (Map.fromList [("k", 2), ("g", 5), ("h", 1)]) -- succeed
 alignLax
   :: (Traversable f, Align.Semialign f) =>
   Prop a ->
@@ -303,6 +367,7 @@
 
 -- | Given a property and a traversable functor-full of values,
 -- succeed if the property succeeds on at least one of the values.
+--
 elem
   :: (HasCallStack, Traversable f) =>
   Prop a ->
@@ -312,7 +377,8 @@
   | otherwise = foldr1 or $ prop <$> values
 
 -- | Given a representable functor-full of properties, and a functor-full of values,
---  yield a representable functor-full of booleans. Similar to `propful`.
+--  yield a representable functor-full of booleans. Similar to 'alignExact'.
+--
 compose ::
   Representable f =>
   f (Prop a) ->
@@ -321,12 +387,16 @@
 compose pr fa = tabulate (\r -> index pr r $ index fa r)
 
 -- | Test all properties against one value.
+--
+-- >>> 1 & checkAll [succeed, equals 2] & failureMessage
+-- Left Actual value 1 but expected 2
+--
 checkAll :: (Foldable f) => f (Prop a) -> Prop a
 checkAll ps a = foldr (\p r -> p a `and` r) (succeed a) ps
 {-# INLINABLE checkAll #-}
 
 -- | Test that a property succeeds against at least one value behind a
--- generalized getter. The corresponding `allOf` is just `traverseOf_`.
+-- generalized getter. The corresponding 'allOf' is just 'Control.Lens.traverseOf_'.
 --
 anyOf
   :: HasCallStack
@@ -338,7 +408,8 @@
   Const vsList = g (Const . pure) vs
 
 -- | Check that a property is true for all values behind a generalized getter
---  and that there's at least one value for which it's true.
+-- and that there's at least one value for which it's true.
+--
 allOf1
   :: (HasCallStack)
   => Getting [a] s a
@@ -351,6 +422,7 @@
   Const vsList = g (Const . pure) vs
 
 -- | A pair of properties, made into a property of pairs.
+--
 pair :: Prop a -> Prop b -> Prop (a, b)
 pair f s (a, b) = f a `and` s b
 
@@ -359,79 +431,97 @@
 fun :: (a -> b) -> PT b a
 fun f p = p . f
 
-fails :: Exception e => Prop e -> Prop (IO a)
-fails p actual = trySync actual >>= \case
+-- | Assert that some computation throws an exception,  and test that the
+-- exception has some property.
+throws :: Exception e => Prop e -> Prop (IO a)
+throws p actual = trySync actual >>= \case
   Left e -> p e
   Right r -> fail "a failed computation" r
 
 -- | Prints the input of a property, if the property fails, using `Show`.
---   Requires that the property's output type can be checked for failure.
+-- Requires that the property's output type can be checked for failure.
 traceFailShow :: Show a => PT a a
 traceFailShow = traceFail show
 
 -- | Prints the input of a property over functions, if the property fails.
---   Requires that the property's output type can be checked for failure.
+-- Requires that the property's output type can be checked for failure.
 traceFail :: (a -> String) -> PT a a
 traceFail s p a =
   assess (p a) $ traceIO (s a)
 
 -- | Internal. Run an extra effect if the input assertion fails.
+--
 assess :: Assertion -> IO () -> Assertion
 assess x eff = trySync @SomeException x >>= either (\ex -> eff >> throwIO ex) return
 
 -- | Prints the input of a property, for debugging.
+--
 traced :: Show a => (a -> String) -> PT a a
 traced s p a = trace (s a) (p a)
 
 -- | Prints the input of a property, for debugging.
+--
 tracedShow :: Show a => PT a a
 tracedShow = traced show
 
 -- | Property which triggers full evaluation of its input and succeeds.
---  Useful for testing that an exception isn't thrown.
+-- Useful for testing that an exception isn't thrown.
 forced :: (NFData a) => Prop a
 forced a = force a `seq` succeed a
 
 -- | The property of being equal to some expected value.
+--
 equals :: (HasCallStack, Eq a) => a -> Prop a
 equals expected actual
   | expected == actual = succeed actual
   | otherwise = fail (PP.pretty (anythingToTextPretty expected)) actual
 
+-- | The property of not being equal to some expected value.
+--
+notEquals :: (HasCallStack, Eq a) => a -> Prop a
+notEquals expected actual
+  | expected /= actual = succeed actual
+  | otherwise = fail ("not equal to " <> PP.pretty (anythingToTextPretty expected)) actual
+
+-- | The property of being less than some expected value.
+--
 lt :: (HasCallStack, Ord a) => a -> Prop a
 lt expected actual
   | actual < expected = succeed actual
   | otherwise = fail ("less than " <> PP.pretty (anythingToTextPretty expected)) actual
 
+-- | The property of being greater than some expected value.
+--
 gt :: (HasCallStack, Ord a) => a -> Prop a
 gt expected actual
   | actual > expected = succeed actual
   | otherwise = fail ("greater than " <> PP.pretty (anythingToTextPretty expected)) actual
 
-gte :: (HasCallStack, Ord a) => a -> Prop a
-gte expected actual
-  | actual >= expected = succeed actual
-  | otherwise = fail ("greater than/equal to " <> PP.pretty (anythingToTextPretty expected)) actual
-
+-- | The property of being less than or equal to some expected value.
+--
 lte :: (HasCallStack, Ord a) => a -> Prop a
 lte expected actual
   | actual <= expected = succeed actual
   | otherwise = fail ("less than/equal to " <> PP.pretty (anythingToTextPretty expected)) actual
 
-bool :: HasCallStack => Bool -> Assertion
-bool b
-  | b = succeed b
-  | otherwise = fail (PP.pretty True) b
+-- | The property of being greater than or equal to some expected value.
+--
+gte :: (HasCallStack, Ord a) => a -> Prop a
+gte expected actual
+  | actual >= expected = succeed actual
+  | otherwise = fail ("greater than/equal to " <> PP.pretty (anythingToTextPretty expected)) actual
 
 -- | Sugar for tupling.
 -- The intended use is something like
--- `(x :: Either Int Int) & branch [match _Left :=> equals 1, match _Right :=> equals 2]`
+-- '(x :: Either Int Int) & branch [match _Left :=> equals 1, match _Right :=> equals 2]'
+--
 pattern (:=>) :: a -> b -> (a, b)
 pattern a :=> b = (a, b)
 infixr 7 :=>
 
--- | Higher precedence '$', to work well with '&'.
--- The intended use is something like `x & match _Right ? equals 2`.
+-- | Higher precedence '$', to work well with 'Data.Function.&'.
+-- The intended use is something like 'x & match _Right ? equals 2'.
+--
 (?) :: (a -> b) -> a -> b
 (?) = ($)
 infixr 8 ?