Document notation

Author: camelid

book/src/glossary.md

@@ -2,6 +2,33 @@
 
 This is a glossary of terminology (possibly) used in the chalk crate.
 
+## Notation
+
+### Basic notation
+
+| Notation     | Meaning                          |
+|--------------|----------------------------------|
+| `?0`         | [Type inference variable]        |
+| `^0`, `^1.0` | [Bound variable]                 |
+| `!0`         | [Placeholder]                    |
+| `A :- B`     | [Clause]; A is true if B is true |
+
+### Rules
+
+- `forall<T> { (Vec<T>: Clone) :- (T: Clone)`: for every `T`, `Vec<T>`
+  implements `Clone` if `T` implements `Clone`
+
+### Queries
+
+- `Vec<i32>: Clone`: does `Vec<i32>` implement `Clone`?
+- `exists<T> { Vec<T>: Clone }`: does there exist a `T` such that `Vec<T>`
+  implements `Clone`?
+
+[Type inference variable]: ../types/rust_types.md#inference-variables
+[Bound variable]: ../types/rust_types.md#bound-variables
+[Placeholder]: ../types/rust_types.md#placeholders
+[Clause]: ../clauses/goals_and_clauses.md
+
 ## Binary connective
 There are sixteen logical connectives on two boolean variables. The most
 interesting in this context are listed below. There is also a truth table given
@@ -50,15 +77,15 @@ the optional positive literal. Due to the equivalence `(P => Q) <=> (!P || Q)`
 the clause can be expressed as `B && C && ... => A` which means that A is true
 if `B`, `C`, etc. are all true. All rules in chalk are in this form. For example
 
-```notrust
+```rust,ignore
 struct A<T> {}
 impl<T> B for A<T> where T: C + D {}
 ```
 
 is expressed as the *Horn clause* `(T: C) && (T: D) => (A<T>: B)`. This formula
 has to hold for all values of `T`. The second example
 
-```notrust
+```rust,ignore
 struct A {}
 impl B for A {}
 impl C for A {}
@@ -149,7 +176,7 @@ syntactic rules.
 In the context of the Rust type system this means that basic rules for type
 construction have to be met. Two examples: 1) Given a struct definition
 
-```notrust
+```rust,ignore
 struct HashSet<T: Hash>
 ```
 then a type `HashSet<i32>` is well-formed since `i32` implements `Hash`. A type