more cleanup

Author: MaximilianAlgehed

docs/Manual.md

@@ -1029,7 +1029,7 @@ ex21 = constrained $ \ d -> width_ d ==. lit 1
 
 
 ## Naming introduced lambda bound Term variables
-1.  [var|name|]
+1.  `[var|name|]`
 
 When we use a library function that introduces new Term variable using a Haskell lambda expression, the system
 gives the Haskell variable a unique Term level name such as `v0` or `v1`  or `v2` etc. When the specification is
@@ -1088,16 +1088,12 @@ Original spec ErrorSpec
 
 
 ## Existential quantifiers
-1.  `exists`
-2.  `unsafeExists`
+1. `exists`
+2. `unsafeExists`
 
-
-Sometimes we want to constrain a variable, in terms of another internal or hidden variable.
-A classic example is constraining a number to be odd.  A number `x` is odd, if there exists
-another internal number `y`, such that, `x` is equal to `y + y + 1`
-
-
-Here is an example.
+Sometimes we want to constrain a variable, in terms of another internal or
+hidden variable.  A classic example is constraining a number to be odd.  A
+number `x` is odd, if there exists a number `y` such that  `x == y + y + 1`:
 
 ```haskell
 ex22 :: Specification Int
@@ -1106,18 +1102,18 @@ ex22 = constrained $ \ [var|oddx|] ->
          (\ [var|y|] -> [Assert $ oddx ==. y + y + 1])
 ```
 
-Why do we call the library function `unsafeExists`? It is unsafe because the library function
-`conformsToSpec` will fail to return `True` when called on a generated result. Why?
-Because the system does not know how to find the internal, hidden variable. To solve this
-the safe function `exists` takes two Haskell lambda expressions.  The first is a function
-that tells how to compute the hidden variable from the values returned by solving the constraints.
-The second is the normal use of a Haskell lambda expression to introduce a Term variable
-naming the hidden variable. Here is an example.
+Why do we call the library function `unsafeExists`? It is unsafe because the
+library function `conformsToSpec` will fail to return `True` when called on a
+generated result. Why?  Because the system does not know how to find the
+hidden variable `y`. To solve this the safe function `exists` takes two
+Haskell lambda expressions. The first is a function that tells how to compute
+the hidden variable from the values returned by solving the constraints. The
+second is the normal use of a Haskell lambda expression to introduce a Term
+variable naming the hidden variable:
 
 ```haskell
 ex23 :: Specification Int
-ex23 = ExplainSpec ["odd via (y+y+1)"] $
-       constrained $ \ [var|oddx|] ->
+ex23 = constrained $ \ [var|oddx|] ->
          exists
 		   -- first lambda, how to compute the hidden value for 'y'
            (\eval -> pure (div (eval oddx - 1) 2))
@@ -1126,19 +1122,21 @@ ex23 = ExplainSpec ["odd via (y+y+1)"] $
            (\ [var|y|] -> [Assert $ oddx ==. y + y + 1])
 ```
 
-One might ask what is the role of the parameter `eval` in the first lambda expression passed to `exists`.
-Recall that we are trying assist the function `conformsToSpec` in determining if a completely known value
-conforms to the specification. In this context, every Term variable is known. But in the specification we
-only have variables with type `(Term a)`,  what we need are variables with type `a`. The `eval` functional parameter
-has type
+One might ask what is the role of the parameter `eval` in the first lambda
+expression passed to `exists`. Recall that we are trying assist the function
+`conformsToSpec` in determining if a _completely known_ value conforms to the
+specification. In this context, every Term variable bound before this point is
+known. But in the specification we only have variables with type `(Term a)`,
+what we need are variables with type `a`. The `eval` functional parameter has
+type:
 
-```haskell
+```
 eval :: Term a -> a
 ```
 
-This, lets us access those values. In the example the Term variable `(oddx :: Term Int)` is in scope, so
+This lets us access those values. In the example the Term variable `(oddx :: Term Int)` is in scope, so
 `(eval oddx :: Int)`, and since this is only used when calling `conformsToSpec`, we actually have the
-value of the `oddx` for `eval` to return. Finally `(div (eval oddx - 1) 2))` tells us how to compute
+value of the `oddx` for `eval` to return. Finally `div (eval oddx - 1) 2` tells us how to compute
 the value of the hidden variable.