More cleanup

Author: MaximilianAlgehed

docs/Manual.md

@@ -192,21 +192,22 @@ sumPair = constrained $ \p ->
       ]
 ```
 
-This example also re-illustrates that `(Term Int)` has a (partial) Num instance, and that we can constrain
-multiple (different) variables using simple `Num` methods (`(+)`, `(-)`, `(*)`, and `negate`). Note also
-the operator: `(==.) :: (Eq n, HasSpec n) => Term n -> Term n -> Term Bool`
+This example also re-illustrates that `(Term Int)` has a (partial) Num
+instance, and that we can constrain multiple (different) variables using simple
+`Num` methods (`(+)`, `(-)`, `(*)`, and `negate`). Note also the operator:
+`(==.) :: (Eq n, HasSpec n) => Term n -> Term n -> Term Bool`
 
 ## Function Symbols
 
-Note that `(<=.)` , and `(==.)` are two of the function symbols in the first order logic. They obey a
-useful naming convention. Infix function symbols corresponding to Haskell infix operators have
-corresponding infix operators,  lifting Haskell infix functions with type `(a -> b -> c)`, to library infix
-functions which have analogous types `(Term a -> Term b -> Term c)`
-and are named using the convention that we add the dot `(.)` to the end of the Haskell operator.
+Note that `(<=.)` and `(==.)` are two of the function symbols in the first
+order logic. They obey a useful naming convention. Infix operators
+corresponding to Haskell infix operators named using the convention that we add
+the dot `(.)` to the end of the Haskell operator.
 
-A similar naming convention holds for function symbols which are not infix, except instead of adding a
-dot to the end of the Haskell name, we add an underscore (`_`) to the end of the Haskell functions's
-name. Some examples follow.
+A similar naming convention holds for normal prefix function symbols,
+except instead of adding a dot to the end of the Haskell name, we add an
+underscore (`_`) to the end of the Haskell functions's name. Some examples
+follow.
 
 ```haskell
 fst_ :: (HasSpec a,HasSpec b) => Term (a,b) -> Term a
@@ -223,7 +224,7 @@ member :: a -> Set a -> Bool
 -- etc
 ```
 
-While the underscored function symbols, may appear to be just to an Applicative
+While the underscored function symbols may appear to be just to an Applicative
 lifting over `Term`, that is not the case. An Applicative lifting would allow
 the base function to be applied under the `Term` type, but the underscored
 function symbols also know how to reason logically about the function and are
@@ -236,9 +237,9 @@ A type with a `HasSpec` instance might have a number of Function Symbols that op
 There are a number of types that have predefined `HasSpec` instances. As a reference, we list them
 here along with the types of their function symbols.
 
-### Function symbols for numeric types
+### Numeric Types
 
-`(Int, Integer, Natural, Int8, Int16, Int32, Int64, Word8, Word16, Word32, Word64)`
+`(Int, Integer, Natural, Int/Word{8, 16, 32, 64})`
 
 The function symbols of numeric types are:
 
@@ -249,24 +250,23 @@ The function symbols of numeric types are:
  5. `(==.) :: (Eq a, HasSpec a) => Term a -> Term a -> Term Bool`
  6.  A partial Num instance for (Term n) where n is a Numeric type. Operators `(+)`, `(-)`, `(*)`
 
-### Function symbols for Bool
+### Booleans
 
 The function symbols of `Bool` are:
 
   1.  `(||.) :: Term Bool -> Term Bool -> Term Bool`  infix `or`
   2.  `not_ :: Term Bool -> Term Bool`
 
-###  Function symbols for List
+### Lists
 
-`HasSpec a => HasSpec [a]`
+We have the instance `HasSpec a => HasSpec [a]`.
 
 The function symbols of `[a]` are:
-
   1.  `foldMap_ :: (Sized [a], Foldy b, HasSpec a) => (Term a -> Term b) -> Term [a] -> Term b`
   2.  `singletonList_ :: (Sized [a], HasSpec a) => Term a -> Term [a]`
   3.  `append_  :: (Sized [a], HasSpec a) => Term [a] -> Term [a] -> Term [a]`
 
-###  Function symbols for Set
+### Sets
 
 `HasSpec a => HasSpec (Set a)`
 
@@ -279,7 +279,7 @@ The function symbols of `(Set a)` are:
   5.  `disjoint_ :: (Ord a, HasSpec a) => Term (Set a) -> Term (Set a) -> Term Bool`
   6.  `fromList_ :: (Ord a, HasSpec a) => Term [a] -> Term (Set a)`
 
-###  Function symbols for Map
+### Maps
 
 `(HasSpec k, HasSpec v) => HasSpec (Map k v)`
 
@@ -296,7 +296,6 @@ Once we have written a `Specification` what can we do with it? Specifications ha
 1.  We can interpret it as a generator of values the meet all the constraints inside the specification.
 2.  We can interpret it as a function that checks if a given value meets all the constraints inside the specification.
 
-
 The first interpretation of the specification is the function `genFromSpec`
 
 ```haskell
@@ -377,7 +376,6 @@ The purpose of constrained generators is to make it possible to write conditiona
 that have a high probability of not being vacuously true, and to combine this with other random
 techniques to make better samples of the test-space.
 
-
 The second interpretation of the specification is as a constraint checker, implemented as the function.
 
 ```haskell