Minor Clean Up

README.md

@@ -29,11 +29,11 @@ Simplicity introduces a groundbreaking low-level programming language and machin
 The distinguishing aspects that set Simplicity apart from conventional programming languages are:
 
 - **Distinct Programming Paradigm**: Simplicity's programming model requires a paradigm shift from conventional programming. It hinges on reasoning about programs in a functional sense with a focus on combinators. This intricacy surpasses even popular functional languages like Haskell, with its own unique challenges.
-- **Exceptional Low-Level Nature**: Unlike high-level languages such as JavaScript or Python, Simplicity operates at an extremely low level, resembling assembly languages. This design choice enables easier reasoning about the formal semantics of programs, but is really work on directly.
+- **Exceptional Low-Level Nature**: Unlike high-level languages such as JavaScript or Python, Simplicity operates at an extremely low level, resembling assembly languages. This design choice enables easier reasoning about the formal semantics of programs, but is rarely worked on directly.
 
 ## SimplicityHL
 
-SimplicityHL is a high-level language that compiles to Simplicity. It maps programming concepts from Simplicity onto programming concepts that developers are more familar with. In particular, Rust is a popular language whose functional aspects fit Simplicity well. SimplicityHL aims to closely resemble Rust.
+SimplicityHL is a high-level language that compiles to Simplicity. It maps programming concepts from Simplicity onto programming concepts that developers are more familiar with. In particular, Rust is a popular language whose functional aspects fit Simplicity well. SimplicityHL aims to closely resemble Rust.
 
 Just how Rust is compiled to assembly language, SimplicityHL is compiled to Simplicity. Just how writing Rust doesn't necessarily produce the most efficient assembly, writing SimplicityHL doesn't necessarily produce the most efficient Simplicity code. The compilers try to optimize the target code they produce, but manually written target code can be more efficient. On the other hand, a compiled language is much easier to read, write and reason about. Assembly is meant to be consumed by machines while Rust is meant to be consumed by humans. Simplicity is meant to be consumed by Bitcoin full nodes while SimplicityHL is meant to be consumed by Bitcoin developers.
 

book/src/function.md

@@ -22,7 +22,7 @@ The function then checks if the carry is true, signaling an overflow, in which c
 On the last line, the value of `sum` is returned.
 
 The above function is called by writing its name `add` followed by a list of arguments `(40, 2)`.
-Each parameter needs an argument, so the list of arguments is as long as the list of arguments.
+Each parameter needs an argument, so the list of arguments is as long as the list of parameters.
 Here, `x` is assigned the value `40` and `y` is assigned the value `2`.
 
 ```rust
@@ -54,7 +54,7 @@ fn level_1() -> u32 {
 }
 
 fn level_2() -> u32 {
-    let (_, next) = jet::increment_32(level_1));
+    let (_, next) = jet::increment_32(level_1());
     next
 }
 ```
@@ -91,7 +91,7 @@ There is no support for "libraries".
 
 ## Jets
 
-Jets are predefined and optimized functions for common usecases.
+Jets are predefined and optimized functions for common use cases.
 
 ```rust
 jet::add_32(40, 2)

book/src/let_statement.md

@@ -48,7 +48,7 @@ let z: u32 = {
     assert!(jet::eq_32(y, 2)); // y == 2
     x
 };
-assert!(jet::eq_32(x, 3)); // z == 3
+assert!(jet::eq_32(z, 3)); // z == 3
 ```
 
 ## Pattern matching

book/src/type.md

@@ -100,11 +100,11 @@ Arrays are always of finite length.
 | `List<A, 256>`            | <256-list           | `list![]`, …, `list![a1, …, a255]`                   |
 | `List<A, 512>`            | <512-list           | `list![]`, …, `list![a1, …, a511]`                   |
 | …                         | …                   | …                                                    |
-| `List<A,`2<sup>N</sup>`>` | <2<sup>N</sup>-list | `list![]`, …, `list![a1, …, a`(2<sup>N</sup> - 1)`]` |
+| `List<A, 2^N>`           | <2^N-list           | `list![]`, …, `list![a1, …, a_{2^N - 1}]`          |
 
 Lists hold a variable number of elements of the same type.
 This is similar to [Rust vectors](https://doc.rust-lang.org/std/vec/struct.Vec.html), but SimplicityHL doesn't have a heap.
-In SimplicityHL, lists exists on the stack, which is why the maximum list length is bounded.
+In SimplicityHL, lists exist on the stack, which is why the maximum list length is bounded.
 
 <2-lists hold fewer than 2 elements, so zero or one element.
 <4-lists hold fewer than 4 elements, so zero to three elements.
@@ -156,7 +156,7 @@ Sum types represent values that are of some "left" type in some cases and that a
 [They work just like in the either crate](https://docs.rs/either/latest/either/enum.Either.html).
 [The Result type from Rust is very similar, too](https://doc.rust-lang.org/std/result/index.html).
 
-A sum type type is generic over two types, `A` and `B`.
+A sum type is generic over two types, `A` and `B`.
 The value `Left(a)` contains an inner value `a` of type `A`.
 The value `Right(b)` contains an inner value `b` of type `B`.
 

book/src/type_casting.md

@@ -57,7 +57,7 @@ All casting in SimplicityHL happens explicitly through a casting expression.
 ```
 
 The above expression casts the value `input` of type `Input` into some output type.
-The input type of the cast is explict while the output type is implicit.
+The input type of the cast is explicit while the output type is implicit.
 
 In SimplicityHL, the output type of every expression is known.
 
@@ -78,4 +78,4 @@ let x: u32 = <(u16, u16)>::into((0, 1));
 ```
 
 In the above example, we cast the tuple `(0, 1)` of type `(u16, u16)` into type `u32`.
-Feel free to consult the table above to verify that this is valid cast.
+Feel free to consult the table above to verify that this is a valid cast.

doc/environment.md

@@ -22,7 +22,7 @@ During the translation, we can ignore the source type of Simplicity expressions
 
 Target types are handled by contexts.
 
-We obtain context Ctx(Ξ) from environment Ξ by mapping each variable `a` from Ξ to the target type of Ξ(`x`):
+We obtain context Ctx(Ξ) from environment Ξ by mapping each variable `x` from Ξ to the target type of Ξ(`x`):
 
 Ctx(Ξ)(`x`) = B if Ξ(`x`) = a: A → B
 
@@ -37,7 +37,7 @@ As we translate `s` to Simplicity, we need an environment that maps the variable
 
 If `p` is just a variable `p = a`, then the environment is simply [`a` ↦ iden: A → A].
 
-If `p` is a product of two variables `p = (a, b)`, then the environment is [`a` ↦ take iden: A × B → A, `b` ↦ drop iden: A × B → B.
+If `p` is a product of two variables `p = (a, b)`, then the environment is [`a` ↦ take iden: A × B → A, `b` ↦ drop iden: A × B → B].
 
 "take" and "drop" are added as we go deeper in the product hierarchy. The pattern `_` is ignored.
 

doc/translation.md

@@ -78,7 +78,7 @@ Then ⟦`b; c`⟧Ξ = comp (pair ⟦`b`⟧Ξ ⟦`c`⟧Ξ) (drop iden): A → C
 
 If Ctx(Ξ) ⊩ `b`: B
 
-If Product(PEnv(B, `p`), Ξ) ⊩ c: C
+If Product(PEnv(B, `p`), Ξ) ⊩ `c`: C
 
 Then ⟦`let p: B = b; c`⟧Ξ = comp (pair ⟦`b`⟧Ξ iden) ⟦`c`⟧Product(PEnv(B, `p`), Ξ): A → C
 
@@ -90,7 +90,7 @@ If Product(PEnv(B, `x`), Ξ) ⊩ `b`: D
 
 If Product(PEnv(C, `y`), Ξ) ⊩ `c`: D
 
-Then ⟦`match a { Left(x) => a, Right(y) => b, }`⟧Ξ = comp (pair ⟦a⟧Ξ iden) (case ⟦b⟧Product(PEnv(B, `x`), Ξ) ⟦c⟧Product(PEnv(C, `y`), Ξ)): A → D
+Then ⟦`match a { Left(x) => b, Right(y) => c, }`⟧Ξ = comp (pair ⟦`a`⟧Ξ iden) (case ⟦`b`⟧Product(PEnv(B, `x`), Ξ) ⟦`c`⟧Product(PEnv(C, `y`), Ξ)): A → D
 
 ## Left unwrap