Tweaks to docs.

docs/01_language_basics.md

@@ -244,7 +244,7 @@ nested functions that can locally capture variables and we also support a
 special parameterized term `fold`:
 
 ```
-fold[f] : ['a -> 'b list] -> 'a
+fold[f] : ['a, 'b list] -> 'a
 ```
 
 where `f` is the name of a function of type `['a, 'b] -> 'a`. Here's an example

docs/04_logical_formulas.md

@@ -138,8 +138,8 @@ thing as `#{"x"}[bool]`.
 ### Built-in formula terms
 
 Formulog provides built-in terms that are used to construct formulas that
-should be interpreted under a particular theory. The formulas generally reflect
-SMT-LIB terms.
+should be interpreted under a particular theory. For the most part, these
+constructors directly reflect the SMT-LIB standard.
 
 #### Parameterized terms
 
@@ -175,10 +175,13 @@ of the bit vectors in the comparisons:
 In this case, one annotation is enough to clarify things:
 
 ```
-`smt_eq[bv[16]](bv_const(42), bv_const(0))`
-`smt_eq(bv_const[16](42), bv_const(0))`
+`smt_eq[bv[32]](bv_const(42), bv_const(0))`
+`smt_eq(bv_const[32](42), bv_const(0))`
 ```
 
+The parameters to a parameterized constructor have to be fully resolved at
+compile time.
+
 #### Logical connectives
 
 Formulog has the standard first-order logic connectives:
@@ -385,7 +388,7 @@ type 'a my_list =
 
 In addition to being able to use the constructors `my_nil` and `my_cons` within
 a formula, one can also use constructors that are automatically generated by
-Formulog and that make it easier to state formula about `my_list` terms:
+Formulog and that make it easier to state formulas about `my_list` terms:
 
 ```
 #is_my_nil  : 'a my_list smt -> bool smt