still more long lines

src/traits-canonical-queries.md

@@ -99,7 +99,8 @@ that the query was false and had no answers (e.g., `Box<i32>: Copy`).
 Otherwise, the `QueryResult` gives back information about the possible answer(s)
 we did find. It consists of four parts:
 
-- **Certainty:** tells you how sure we are of this answer. It can have two values:
+- **Certainty:** tells you how sure we are of this answer. It can have two
+  values:
   - `Proven` means that the result is known to be true.
     - This might be the result for trying to prove `Vec<i32>: Clone`,
       say, or `Rc<?T>: Clone`.
@@ -171,7 +172,8 @@ Therefore, the result we get back would be as follows (I'm going to
 ignore region constraints and the "value"):
 
 - Certainty: `Ambiguous` -- we're not sure yet if this holds
-- Var values: `[?T = ?T, ?U = ?U]` -- we learned nothing about the values of the variables
+- Var values: `[?T = ?T, ?U = ?U]` -- we learned nothing about the values of
+  the variables
 
 In short, the query result says that it is too soon to say much about
 whether this trait is proven. During type-checking, this is not an

src/traits-canonicalization.md

@@ -129,8 +129,8 @@ for which we made a substutition S:
 
     S = [?A, '?B, ?C]
     
-We then did some work which unified some of those variables with other things. If we
+We then did some work which unified some of those variables with other things.
-"refresh" S with the latest results, we get:
+If we "refresh" S with the latest results, we get:
 
     S = [Vec<?E>, '?D, ?E]
     

src/traits-goals-and-clauses.md

@@ -81,13 +81,15 @@ Given that, we can define a `DomainGoal` as follows:
   - as we'll see in the section on lowering, `FromEnv(X)` implies
     `Implemented(X)` but not vice versa. This distinction is crucial
     to [implied bounds].
-- `ProjectionEq(Projection = Type)` -- the given associated type `Projection` is equal
+- `ProjectionEq(Projection = Type)` -- the given associated type `Projection`
-  to `Type`; see [the section on associated types](./traits-associated-types.html)
+  is equal to `Type`; see [the section on associated
+  types](./traits-associated-types.html)
   - in general, proving `ProjectionEq(TraitRef::Item = Type)` also
     requires proving `Implemented(TraitRef)`
-- `Normalize(Projection -> Type)` -- the given associated type `Projection` can be [normalized][n]
+- `Normalize(Projection -> Type)` -- the given associated type `Projection` can
-  to `Type`
+  be [normalized][n] to `Type`
-  - as discussed in [the section on associated types](./traits-associated-types.html),
+  - as discussed in [the section on associated
+    types](./traits-associated-types.html),
     `Normalize` implies `ProjectionEq` but not vice versa
 - `WellFormed(..)` -- these goals imply that the given item is
   *well-formed*

src/traits-lowering-rules.md

@@ -26,7 +26,7 @@ Each of these lowering rules is given a name, documented with a
 comment like so:
 
     // Rule Foo-Bar-Baz
-    
+
 you can also search through the `librustc_traits` crate in rustc
 to find the corresponding rules from the implementation.
 
@@ -36,7 +36,8 @@ When used in a goal position, where clauses can be mapped directly to
 [domain goals][dg], as follows:
 
 - `A0: Foo<A1..An>` maps to `Implemented(A0: Foo<A1..An>)`.
-- `A0: Foo<A1..An, Item = T>` maps to `ProjectionEq(<A0 as Foo<A1..An>>::Item = T)`
+- `A0: Foo<A1..An, Item = T>` maps to
+  `ProjectionEq(<A0 as Foo<A1..An>>::Item = T)`
 - `T: 'r` maps to `Outlives(T, 'r)`
 - `'a: 'b` maps to `Outlives('a, 'b)`
 
@@ -58,7 +59,7 @@ on the lowered where clauses, as defined here:
 - `WellFormed(WC)` -- this indicates that:
   - `Implemented(TraitRef)` becomes `WellFormed(TraitRef)`
   - `ProjectionEq(Projection = Ty)` becomes `WellFormed(Projection = Ty)`
-  
+
 *TODO*: I suspect that we want to alter the outlives relations too,
 but Chalk isn't modeling those right now.
 
@@ -106,7 +107,7 @@ The next few clauses have to do with implied bounds (see also
     forall<Self, P1..Pn> {
       FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn)
     }
-    
+
 This clause says that if we are assuming that the trait holds, then we can also
 assume that it's where-clauses hold. It's perhaps useful to see an example:
 
@@ -125,12 +126,14 @@ clauses** but also things that follow from them.
 The next rule is related; it defines what it means for a trait reference
 to be **well-formed**:
 
-    // Rule WellFormed-TraitRef
+```txt
-    //
+// Rule WellFormed-TraitRef
-    // For each where clause WC:
+//
-    forall<Self, P1..Pn> {
+// For each where clause WC:
-      WellFormed(Self: Trait<P1..Pn>) :- Implemented(Self: Trait<P1..Pn>) && WellFormed(WC)
+forall<Self, P1..Pn> {
-    }
+  WellFormed(Self: Trait<P1..Pn>) :- Implemented(Self: Trait<P1..Pn>) && WellFormed(WC)
+}
+```
 
 This `WellFormed` rule states that `T: Trait` is well-formed if (a)
 `T: Trait` is implemented and (b) all the where-clauses declared on
@@ -149,9 +152,9 @@ trait A { }
 trait B { }
 ```
 
-Here, the transitive set of implications for `T: Foo` are `T: A`, `T: Bar`, and `T: B`.
+Here, the transitive set of implications for `T: Foo` are `T: A`, `T: Bar`, and
-And indeed if we were to try to prove `WellFormed(T: Foo)`, we would have to prove each
+`T: B`.  And indeed if we were to try to prove `WellFormed(T: Foo)`, we would
-one of those:
+have to prove each one of those:
 
 - `WellFormed(T: Foo)`
   - `Implemented(T: Foo)`
@@ -212,7 +215,7 @@ but reproduced here for reference:
         Implemented(Self: Trait<P1..Pn>)
         && WC1
     }
-    
+
 The next rule covers implied bounds for the projection. In particular,
 the `Bounds` declared on the associated type must be proven to hold to
 show that the impl is well-formed, and hence we can rely on them
@@ -223,8 +226,8 @@ elsewhere.
 
 ### Lowering function and constant declarations
 
-Chalk didn't model functions and constants, but I would eventually
+Chalk didn't model functions and constants, but I would eventually like to
-like to treat them exactly like normalization. See [the section on function/constant
+treat them exactly like normalization. See [the section on function/constant
 values below](#constant-vals) for more details.
 
 ## Lowering impls
@@ -272,7 +275,7 @@ We produce the following rule:
           WC && WC1
       }
     }
-  
+
 Note that `WC` and `WC1` both encode where-clauses that the impl can
 rely on.