fix nits

Author: nikomatsakis

book/src/recursive.md

@@ -10,11 +10,11 @@ fn(Goal) -> Solution
 where the Goal is some [canonical goal](./canonical_queries.md) and
 the Solution is a result like:
 
-* Provable(S): meaning the goal is provable and it is provably exactly (and only
-  for the substitution S. S is a set of values for the inference variables that
-  appear in the goal. So if we had a goal like `Vec<?X>: Foo`, and we returned
-  `Provable(?X = u32)`, it would mean that only `Vec<u32>: Foo` and not any
-  other sort of vector (e.g., `Vec<u64>: Foo` does not hold).
+* Provable(S): meaning the goal is provable and it is provably exactly (and
+  only) for the substitution S. S is a set of values for the inference variables
+  that appear in the goal. So if we had a goal like `Vec<?X>: Foo`, and we
+  returned `Provable(?X = u32)`, it would mean that only `Vec<u32>: Foo` and not
+  any other sort of vector (e.g., `Vec<u64>: Foo` does not hold).
 * Ambiguous(S): meaning that we can't prove whether or not the goal is true.
   This can sometimes come with a substitution S, which offers suggested values
   for the inference variables that might make it provable.
@@ -40,20 +40,20 @@ Implemented(u32: A)
 Implemented(i32: A)
 ```
 
-Now, suppose that we have a goal like `Implemented(Vec<f32>: A)`. This would
+First, suppose that we have a goal like `Implemented(Vec<u64>: A)`. This would
 proceed like so:
 
-* `Solve(Implemented(Vec<f32>: A))`
-    * `Solve(Implemented(f32: A))`
+* `Solve(Implemented(Vec<u64>: A))`
+    * `Solve(Implemented(u64: A))`
         * returns `Error`
     * returns `Error`
 
 In other words, the recursive solver would start by applying the first rule,
-which would cause us recursively try to solve `Implemented(f32: A)`. This would
+which would cause us recursively try to solve `Implemented(u64: A)`. This would
 yield an Error result, because there are no applicable rules, and that error
-would propagae back up, causing the entire attempt at proving things to fail.
+would propagate back up, causing the entire attempt at proving things to fail.
 
-Now consider `Implemented(Vec<u32>: A)`. This would proceed like so:
+Next, consider `Implemented(Vec<u32>: A)`. This would proceed like so:
 
 * `Solve(Implemented(Vec<u32>: A))`
     * `Solve(Implemented(u32: A))`
@@ -90,8 +90,8 @@ In the recursive solver, with a goal of `Implemented(Vec<?X>: A)`, we
 recursively try to prove `Implemented(?X: A)` and get ambiguity, and we get
 stuck there.
 
-The SLG solver in contrast starts by exploring `?X = u32` and finds
+The [SLG solver] in contrast starts by exploring `?X = u32` and finds
 that it works, and then later tries to explore `?X = i32` and finds that it
 fails (because `i32: B` is not true).
 
-[slg solver]: ./engine.md
+[SLG solver]: ./engine.md

book/src/recursive/inductive_cycles.md

@@ -80,11 +80,12 @@ to the same goal, S and S1. This implies two possibilities:
   and in fact we can just stop and return right now.
 
 This technique is very similar to the traditional Prolog technique of handling
-cycles, which is called **tabling**. The difference between our solution and
-table is that we are always looking for a unique solution, whereas Prolog (like
-the [SLG solver]) tries to enumerate all solutions (i.e., in prolog, solving a
-goal is not a function but an iterator that yields solutions, and hence it would
-yield up S first, and then S1, and then any further answers we might get).
+cycles, which is called **tabling**. The difference between our approach and
+tabling is that we are always looking for a unique solution, whereas Prolog
+(like the [SLG solver]) tries to enumerate all solutions (i.e., in Prolog,
+solving a goal is not a function but an iterator that yields solutions, and
+hence it would yield up S first, and then S1, and then any further answers we
+might get).
 
 [SLG solver]: ../engine.md
 

book/src/recursive/search_graph.md

@@ -12,11 +12,11 @@ actually implement this? That's where the [`SearchGraph`] comes into play.
 [`Node`]: http://rust-lang.github.io/chalk/chalk_solve/recursive/search_graph/struct.Node.html
 [`stack_depth`]: http://rust-lang.github.io/chalk/chalk_solve/recursive/search_graph/struct.Node.html#structfield.stack_depth
 
-The role of the [`SearchGraph`] is to store information each goal that we are
-currently solving. Typically, these are goals on the stack -- but other times,
-they are goals that are no longer on the stack, but whose results (because of a
-cycle) were dependent on something that is still on the stack. We'll work
-through some examples to make it all clear.
+The role of the [`SearchGraph`] is to store information about each goal that we
+are currently solving. Typically, these are goals on the stack -- but other
+times, they are goals that are no longer on the stack, but whose results
+(because of a cycle) were dependent on something that is still on the stack.
+We'll work through some examples to make it all clear.
 
 
 ## Structure of the search graph

book/src/recursive/stack.md

@@ -68,7 +68,9 @@ one of the bits of information is the [`StackDepth`] of its entry on the stack
 (if any).
 
 Therefore, when we are about to start solving some (canonical) goal G, we can
-detect a cycle by checking in the searh graph to see whether G has an associated
+detect a cycle by checking in the [search graph] to see whether G has an associated
 [`StackDepth`]. If so, it must be on the stack already (and we can set the
 [`cycle`] field to true...but I get ahead of myself, read the next chapters
 to learn more about that).
+
+[search graph]: ./search_graph.md