Fix some book typos

book/src/canonical_queries/canonicalization.md

@@ -143,7 +143,7 @@ when first instantiating our query. To refresh your memory, we had a query
 for<T,L,T> { ?0: Foo<'?1, ?2> }
 ```
 
-for which we made a substutition S:
+for which we made a substitution S:
 
 ```text
 S = [?A, '?B, ?C]

book/src/clauses/coherence.md

@@ -81,7 +81,7 @@ Given an impl of the form `impl<T0…Tn> Trait<P1…Pn> for P0`, the impl is all
         - This only really applies if we allowed fundamental types with multiple type parameters
         - Since we don’t do that yet, we can ignore this for the time being
     - All types `Pj` such that `j < i` do not contain `T0…Tn` at any level of depth (i.e. the types are **fully visible** **—** “visible” meaning that the type is a known type and not a type parameter or variable)
-## Modelling The Orphan Check
+## Modeling The Orphan Check
 
 Determining how to model these rules in chalk is actually quite straightforward at this point. We have an exact specification of how the rules are meant to work and we can translate that directly. 
 
@@ -122,7 +122,7 @@ forall<Self, P1...Pn> {
     IsLocal(Pn)
 }
 ```
-Here, we have modelled every possible case of `P1` to `Pn` being local and then checked if all prior type parameters are fully visible. This truly is a direct translation of the rules listed above!
+Here, we have modeled every possible case of `P1` to `Pn` being local and then checked if all prior type parameters are fully visible. This truly is a direct translation of the rules listed above!
 
 Now, to complete the orphan check, we can iterate over each impl of the same form as before and check if `LocalImplAllowed(P0: Trait<P1…Pn>)` is provable.
 
@@ -166,7 +166,7 @@ The conclusion from all of this is that it is perfectly safe to rule out impls t
 
 **Downstream Crates:** Downstream crates come into play because all traits in upstream crates and in the current crate can potentially be implemented by downstream crates using the forms allowed by the orphan rules. In essence, we always need to assume that downstream crates will implement traits in all ways that compile.
 
-## Discussion: Modelling the Overlap Check
+## Discussion: Modeling the Overlap Check
 
 [Aaron’s excellent blog post](https://aturon.github.io/blog/2017/04/24/negative-chalk/) talks about this exact problem from the point of view of negative reasoning. It also describes a potential solution which we will apply here to solve our problem.
 
@@ -240,7 +240,7 @@ forall<T> { DownstreamType(MyFundamentalType<T>) :- DownstreamType(T) }
 
 ## Overlap Check in Chalk
 
-Thus, based on the discussion above, the overlap check with coherence in mind can be modelled in chalk with the following:
+Thus, based on the discussion above, the overlap check with coherence in mind can be modeled in chalk with the following:
 
 
 - All disjoint queries take place inside of `compatible`
@@ -318,7 +318,7 @@ Initially, when Niko and I started working on this, Niko suggested the following
 > }
 > ```
 
-This appears to make sense because we need to assume that any impls that the current crate cannot add itself may exist somewhere else. By using `not { LocalImplAllowed(…) }`, we modelled exactly that. The problem is, that this assumption is actually too strong. What we actually need to model is that any **compatible** impls that the current crate cannot add itself may exist somewhere else. This is a **subset** of the impls covered by `not { LocalImplAllowed(…) }`.
+This appears to make sense because we need to assume that any impls that the current crate cannot add itself may exist somewhere else. By using `not { LocalImplAllowed(…) }`, we modeled exactly that. The problem is, that this assumption is actually too strong. What we actually need to model is that any **compatible** impls that the current crate cannot add itself may exist somewhere else. This is a **subset** of the impls covered by `not { LocalImplAllowed(…) }`.
 
 Notes to be added somewhere:
 

book/src/clauses/implied_bounds.md

@@ -183,7 +183,7 @@ of  "local" implied bound reasoning which would say
 only be done within our `foo` function in order to avoid the earlier
 problem where we had a global clause.
 
-We can apply these local reasonings everywhere we can have an environment
+We can apply this local reasoning everywhere we can have an environment
 -- i.e. when we can write where clauses -- that is, inside impls,
 trait declarations, and type declarations.
 

book/src/clauses/opaque_types.md

@@ -65,7 +65,7 @@ A chalk opaque type declaration has several parts:
 * The **generic parameters** `P0..Pn`. In real Rust, these parameters are inherited
   from the context in which the `impl Trait` appeared. In our example, these
   parameters come from the surrounding function. Note that in real Rust the set
-  of generic parmaeters is a *subset* of those that appear on the surrounding
+  of generic parameters is a *subset* of those that appear on the surrounding
   function: in particular, lifetime parameters may not appear unless they explicitly
   appear in the opaque type's bounds.
 * The **bounds**, which would be `IntoIterator<Item = u32> + 'a` in our example.
@@ -75,7 +75,7 @@ A chalk opaque type declaration has several parts:
 * The **where clauses**, which would be `T: Copy` and `T: Into<u32>` in our
   example. These are conditions that must hold on `V0..Vn` for
   `OpaqueTypeName<V0..Vn>` to be a valid type.
-    * Note that constrast with bounds: bounds are things that the hidden type must meet
+    * Note that this contrasts with bounds: bounds are things that the hidden type must meet
       but which the rest of the code can assume to be true. Where clauses are things
       that the rest of the code must prove to be true in order to use the opaque type.
       In our example, then, a type like `AsU32sReturn<'a, String>` would be invalid

book/src/engine.md

@@ -8,7 +8,7 @@ Rust types, or Rust logic.
 
 The engine implements the following PROLOG logic concepts. Some of these
 have been published on previously, and some are `Chalk`-specific. This isn't
-necesarily an exhaustive list:
+necessarily an exhaustive list:
 - Basic logic
 - Negation
 - Floundering
@@ -18,6 +18,6 @@ necesarily an exhaustive list:
 
 Throughout most of this chapter, the specifics in regards to
 `Canonicalization` and `UCanonicalization` are avoided. These are important
-concepts to understand, but don't particulary help to understand how
+concepts to understand, but don't particularly help to understand how
 `chalk-engine` *works*. In a few places, it may be highlighted if it *is*
 important.

book/src/engine/logic.md

@@ -32,7 +32,7 @@ As either `Answer`s are found for the selected `Table`, entries on the stack are
 
 ## Table creation
 
-As mentioned before, whenever a new `Goal` is encounted, a new [`Table`] is
+As mentioned before, whenever a new `Goal` is encountered, a new [`Table`] is
 created to store current and future answers. First, the [`Goal`] is converted into
 an `HhGoal`. If it can be simplified, then a `Strand` with one or more
 subgoals will be generated and can be followed as above. Otherwise, if it is a
@@ -86,7 +86,7 @@ anywhere.
 ## Cycles
 
 If while pursuing a `Goal`, the engine encounters the same `Table` twice, then a
-cycle has occured. If the cycle is not coinductive (see next), then there is
+cycle has occurred. If the cycle is not coinductive (see next), then there is
 nothing that can be gained from taking this route. We mark how far up the stack
 is in the cycle, and try the next `Strand`. If all `Strand`s for a table
 encounter a cycle, then we know that the current selected `Goal` has no more

book/src/engine/logic/coinduction.md

@@ -17,7 +17,7 @@ What happens is that we
 
 * start to prove C1
 * start to prove C2
-* see a recursive attempt to prove C1, assume it is succesful
+* see a recursive attempt to prove C1, assume it is successful
 * consider C2 proved **and cache this**
 * start to prove C3, fail
 * consider C1 **unproven**
@@ -92,7 +92,7 @@ This is true for all `A, B`
 ### High-level idea
 
 * When we encounter a co-inductive subgoal, we delay them in the current `Strand`
-* When all subgoals have been tested, and there are remaining delayed co-inductive subgoals, this is propogated up, marking the current `Strand` as co-inductive
+* When all subgoals have been tested, and there are remaining delayed co-inductive subgoals, this is propagated up, marking the current `Strand` as co-inductive
 * When the co-inductive `Strand`s reach the root table, we only then pursue an answer
 
 ## Niko's proposed solution
@@ -195,7 +195,7 @@ I think when we get a new answer, we want it to *overwrite* the old answer in pl
 
 In particular, it could be that the table already has a "complete" set of answers -- i.e., somebody invoked `ensure_answer(N)` and got back `None`. We don't want to be adding new answers which would change the result of that call. It *is* a bit strange that we are changing the result of `ensure_answer(i)` for the current `i`, but then the result is the same answer, just a bit more elaborated.
 
-The idea then would be to create a strand *associated with this answer somehow* (it doesn't, I don't think, live in the normal strand table; we probably have a separate "refinment strand" table). This strand has as its subgoals the delayed subgoals. It pursues them. This either results in an answer (which replaces the existing answer) or an error (in which case the existing answer is marked as *error*). This may require extending strand with an optional answer index that it should overwrite, or perhaps we thread it down as an argument to `pursue_strand` (optional because, in the normal mode, we are just appending a new answer).
+The idea then would be to create a strand *associated with this answer somehow* (it doesn't, I don't think, live in the normal strand table; we probably have a separate "refinement strand" table). This strand has as its subgoals the delayed subgoals. It pursues them. This either results in an answer (which replaces the existing answer) or an error (in which case the existing answer is marked as *error*). This may require extending strand with an optional answer index that it should overwrite, or perhaps we thread it down as an argument to `pursue_strand` (optional because, in the normal mode, we are just appending a new answer).
 
 (Question: What distinguishes root answer? Nothing -- we could actually do this process for any answer, so long as the delayed subgoals are not to tables actively on the stack. This just happens to be trivially true for root answers. The key part though is that the answer must be registered in the table first before the refinement strand is created, see Delayed Self-Cycle Variant 3.)
 

book/src/engine/slg.md

@@ -252,7 +252,7 @@ Since we now have an answer, `ensure_answer(T1, A0)` will return `Ok`
 to the table T0, indicating that answer A0 is available. T0 now has
 the job of incorporating that result into its active strand. It does
 this in two ways. First, it creates a new strand that is looking for
-the next possible answer of T1. Next, it incorpoates the answer from
+the next possible answer of T1. Next, it incorporates the answer from
 A0 and removes the subgoal. The resulting state of table T0 is:
 
 ```text

book/src/glossary.md

@@ -59,11 +59,11 @@ Examples for binders:
 - A sum `\sum_n x_n` binds the index variable `n`.
 
 ## Canonical Form
-A formula in canonical form has the property that its DeBruijn indices are
+A formula in canonical form has the property that its De Bruijn indices are
 minimized. For example when the formula `forall<0, 1> { 0: A && 1: B }` is
 processed, both "branches" `0: A` and `1: B` are processed individually. The
 first branch would be in canonical form, the second branch not since the
-occurring DeBruijn index `1` could be replaced with `0`.
+occurring De Bruijn index `1` could be replaced with `0`.
 
 ## Clause
 A clause is the disjunction of several expressions. For example the clause
@@ -95,8 +95,8 @@ impl C for A {}
 is expressed as the *Horn clause* `(A: B) && (A: C)`. Note the missing
 consequence.
 
-## DeBruijn Index
-DeBruijn indices numerate literals that are bound in an unambiguous way. The
+## De Bruijn Index
+De Bruijn indices numerate literals that are bound in an unambiguous way. The
 literal is given the number of its binder. The indices start at zero from the
 innermost binder increasing from the inside out.
 
@@ -105,7 +105,7 @@ literal names `U` and `T` are replaced with `0` and `1` respectively and the nam
 { exists<_> { 1: Foo<Item=0> } }`.
 
 As another example, in `forall<X, Y> { forall <Z> { X } }`, `X` is represented
-as `^1.0`. The `1` represents the de Bruijn index of the variable and the `0`
+as `^1.0`. The `1` represents the De Bruijn index of the variable and the `0`
 represents the index in that scope: `X` is bound in the second scope counting
 from where it is referenced, and it is the first variable bound in that scope.
 
@@ -127,7 +127,7 @@ goal.
 
 ## Normal form
 To say that a statement is in a certain *normal form* means that the pattern in
-which the subformulas are arranged fulfil certain rules. The individual patterns
+which the subformulas are arranged fulfill certain rules. The individual patterns
 have different advantages for their manipulation.
 
 ### Conjunctive normal form (CNF)

book/src/types/operations/fold.md

@@ -59,7 +59,7 @@ Thus, as a user, you can customize folding by:
 ## The `binders` argument
 
 Each callback in the [`Folder`] trait takes a `binders` argument. This indicates
-the number of binders that we have traversed during folding, which is relevant for debruijn indices.
+the number of binders that we have traversed during folding, which is relevant for De Bruijn indices.
 So e.g. a bound variable with depth 1, if invoked with a `binders` value of 1, indicates something that was bound to something external to the fold.
 
 XXX explain with examples and in more detail

book/src/types/rust_types.md

@@ -142,7 +142,7 @@ them in the [aliases chapter](./rust_types/alias.md).
 The `BoundVar` variant represents some variable that is bound in
 an outer term. For example, given a term like `forall<X> {
 Implemented(X: Trait) }`, the `X` is bound. Bound variables in chalk
-(like rustc) use de bruijin indices (See below).
+(like rustc) use De Bruijn indices (See below).
 
 Bound variables are never directly equated, as any bound variables would have
 been instantiated with either inference variables or placeholders.

book/src/types/rust_types/application_ty.md

@@ -23,14 +23,14 @@ A `Generator` represents a Rust generator. There are three major components
 to a generator:
 
 * Upvars - similar to closure upvars, they reference values outside of the generator,
-  and are stored across al yield points.
+  and are stored across all yield points.
 * Resume/yield/return types - the types produced/consumed by various generator methods.
   These are not stored in the generator across yield points - they are only
   used when the generator is running.
 * Generator witness - see the `Generator Witness` section below.
 
 Of these types, only upvars and resume/yield/return are stored directly in `GeneratorDatum`
-(which is acessed via `RustIrDatabase`). The generator witness is implicitly associated with
+(which is accessed via `RustIrDatabase`). The generator witness is implicitly associated with
 the generator by virtue of sharing the same `GeneratorId`. It is only used when determining
 auto trait impls, where it is considered a 'constituent type'.