meow

1 files changed, 26 insertions, 27 deletions

diff --git a/plt/lean.md b/plt/lean.md
index 9aae9fa..a7d0b86 100644
--- a/plt/lean.md
+++ b/plt/lean.md
@@ -180,7 +180,7 @@ The best way to find out what you're looking at is to use VS Code's right-click
 
 The `structure` type is analogous to structs in other languages. It behaves much as one would expect.
 
-```lean
+```haskell
 structure Header where
   (width height : Nat)
   alpha : Bool
@@ -205,13 +205,13 @@ Structures may be constructed with braces. The braces are syntactic sugar for an
 Structures may be destructured either by pattern matching or with dot notation for field access. Pattern matching may be done via `match` or inline via `let` with the `{}` syntax.
 
 They cannot be mutated: Lean is functional and so there is no explicit syntax for updating a field. `header.width ← ...` does nothing, even if `header` is declared to be mutable. Instead, the entire `header` structure must be updated at once. This can be a pain on large structures, so Lean provides the `with` keyword for succiently (re-)constructing a structure with only a few fields changed. The `increment_height` function above can thus be compactly declared as the following:
-```lean
+```haskell
 def increment_height (header : Header) : Header :=
   { header with height := header.height + 1 }
 ```
 
 Structures may *extend* one another. A structure inherits all the fields of the structures it extends (which must not conflict), and can declare new fields. Default values may be redefined but fields may not be. As a type may not be referenced before its declaration, cyclic extensions cannot be formed.
-```lean
+```haskell
 structure Point where
   (x y : Int)
 
@@ -235,8 +235,8 @@ See also: [FPIL:Structures](https://leanprover.github.io/functional_programming_
 
 Sometimes, it is convenient to not need to bother with naming structures or their fields. Whether inline within the definition of a more complex type, or as the return type of a helper function, it can be the case that having explicit names is more trouble than it is worth.
 
-Lean provides a type for *anonymous structures*, that behave in a very similar fashion to *tuples* in other languages. This is called `Prod` on analogy with `Sum` (which we will see later) and is defined as follows:
-```lean
+Lean provides a type for *anonymous structures*, that behave in a very similar fashion to *tuples* in other languages. This is called `Prod` on analogy with `Sum` (which we will see later).
+```haskell
 structure Prod (α : Type) (β : Type) where
   fst : α
   snd : β
@@ -259,10 +259,8 @@ See also: [FPIL:Polymorphism#Prod](https://leanprover.github.io/functional_progr
 
 ### Sums
 
-Similarly to [products](#products), it is sometimes convenient to not need to bother with naming inductives or their variants.
-
-The `Sum` type provides for this. It is defined as follows:
-```lean
+Similarly to [products](#products), it is sometimes convenient to not need to bother with naming inductives or their variants. The `Sum` type provides for this.
+```haskell
 inductive Sum (α : Type) (β : Type) where
   | inl (val : α)
   | inr (val : β)
@@ -275,7 +273,7 @@ See also: [FPIL/Polymorphism#Sum](https://lean-lang.org/functional_programming_i
 ### Booleans
 
 Lean provides a `Bool` type, defined as an inductive data type:
-```lean
+```haskell
 inductive Bool where
   | false
   | true
@@ -284,17 +282,18 @@ inductive Bool where
 The `true` and `false` terms are exported in the Prelude and do not need to be prefixed with `Bool`. Standard `if`/`else` destructors are also provided. `else if` is special cased in the parser to behave nicely.
 
 `if` is also overloaded to function with `let` to provide a compact alternative to a `match` statement.
-```lean
+```haskell
 let a := Chunk.rgb 1 2 3
 if let {r, g, b} := a then
   IO.println s!"red: {r}, green: {g}, blue: {b}"
+```
 
 ### Numbers
 
 Lean provides a variety of representations of numbers. The main three are [`Nat`], [`Int`], and [`Fin n`].
 
 `Nat` is an arbitrary-sized number type. It is defined as the following:
-```lean
+```haskell
 -- Zero is a natural number.
 -- The successor of a natural number is a natural number.
 inductive Nat where
@@ -307,7 +306,7 @@ Lean recognizes numeric literals (`0`, `1`, `2`...) as numeric constructors, equ
 It should be noted that Lean treats operations on `Nat` that would produce a negative number **as producing zero**. For example, `#check 4 - 5` prints `4 - 5 : Nat`, and `#eval 4 - 5` prints `0`.
 
 [`Int`] is an extension of `Nat` to also represent negative numbers. It is similarly special-cased by the compiler. Lean recognizes (..., `-2`, `-1`) as equivalent to their `Int.negSucc n` counterparts, and will also implicitly cast (`0`, `1`, `2`...) to `Int` as required.
-```lean
+```haskell
 -- A natural number is an integer.
 -- The negation of the *successor* of a natural number is an integer.
 -- (the above is enforced by compiler magic)
@@ -317,7 +316,7 @@ inductive Int where
 ```
 
 [`Fin n`] is a natural number guaranteed to be *smaller* than `n`: i.e. `i ∈ ℕ : 0 ≤ i < n`. The underlying representation is `val : Nat` and a proof that the `val < n`.
-```lean
+```haskell
 -- If i : Fin n, then i.val : Nat is the described number.
 -- It can also be written as i.1 or just i when the target type is known.
 -- If i : Fin n, then i.isLt is a proof that i.val < n.
@@ -329,7 +328,7 @@ structure Fin (n : Nat) where
 Lean supports the following fixed-width integers: [`UInt8`], [`UInt16`], [`UInt32`], [`UInt64`], [`USize`]. They behave as one would expect. `USize` takes the size of a pointer on its appropriate platforms. Lean also supports *arbitrary* fixed-width integers with [`BitVec w`]. They are treated internally as `Fin (2 ^ w)`, and gain all the special support for math that `Fin n` and subsequently `Nat` has.
 
 Lean is good at typechecking numbers. For example, the following code compiles:
-```lean
+```haskell
 abbrev UInt6 := BitVec 6
 structure Pixel where
   (r g b a : UInt8)
@@ -341,9 +340,9 @@ def hash (pixel : Pixel) : UInt6 :=
 
 The expected basic mathematical operations are defined on all numbers. Their semantics differ depending on the specific numeric type.
 - arithmetic: `+`, `-`, `*`, `/`, `%`, `∣`
-- comparison: `<`, `>`, `<=`/`≤`, `>=`/`≥`
+- comparison: `<`, `>`, `<=` and `≤`, `>=` and `≥`
 - bitwise: `&&&`, `|||`, `^^^`, `~~~`
-- shifts: `<<<` and `>>>`
+- shifts: `<<<`, `>>>`
 
 Numbers regularly need to be explicitly converted between different representations. This may be done via various `.toType` and `.ofType` methods.
 
@@ -352,7 +351,7 @@ Numbers regularly need to be explicitly converted between different representati
 Lean provides for several representations of list-like data structures.
 
 [`List α`] is the standard representation. It is represented as a linked list, and defined as the following:
-```lean
+```haskell
 inductive List (α : Type u) where
   | nil
   | cons (head : α) (tail : List α)
@@ -360,15 +359,15 @@ inductive List (α : Type u) where
 
 `List.nil` or more commonly `[]` represents the empty list. `List.cons a l` or `a :: l` (for some `a : α`, `l : List α`) are used for list concatenation. `[a, b, c, ...]` syntax can also be used for construction of lists. Various functions and classes are defined for and on lists.
 
-[`Array α`] is isomorphic to `List α`. It is represented as a dynamic array. `Arrays` are significantly more performant than `Lists`: not only are they more efficient at everything except insertation and deletion, but so long as arrays are used "linearly", all updates will be *destructive* - which provides comparable performance to mutable arrays in imperative programming languages.
+[`Array α`] is isomorphic to `List α`. It is represented as a dynamic array. Arrays are significantly more performant than Lists: not only are they more efficient at everything except insertation and deletion, but so long as arrays are used "linearly", all updates will be *destructive* - which provides comparable performance to mutable arrays in imperative programming languages. As such, you usually want to use `Array`.
 
-You usually want to use `Array`. However: currently `Arrays` are represented as an array of *pointers* in memory, for ABI reasons. This is an obvious performance pitfall and liable to change in the (near) future. But for now, Lean provides special [`ByteArray`] / [`FloatArray`] types that are treated like `Array UInt8` and `Array Float` respectively, but represented as real unboxed byte/float arrays.
+However: currently `Arrays` are represented as an array of *pointers* in memory, for ABI reasons. This is an obvious performance pitfall and liable to change in the (near) future. But for now, Lean provides special [`ByteArray`] / [`FloatArray`] types that are treated like `Array UInt8` and `Array Float` respectively, but represented as real unboxed byte/float arrays.
 
 `Array` has a different syntax for its constructor: `#[a, b, c]`. It does overload `a :: l`.
 
 The [`Batteries.Vector α n`] type is not in `Std`, but worth a mention. It is a *statically sized array*: represented under the hood by `Array`, but guaranteed to not change size throughout its existence.
 
-All lists provide postfix `foo[i]` syntax for accessing arbitrary array elements. There are three variations:
+All lists provide some postfix `foo[i]` syntax for accessing arbitrary array elements.
 - `foo[i]` takes an `i : Fin n`, where `n < foo.size`. If this cannot be proven it fails to compile.
 - `foo[i]?` returns an `Option α`.
 - `foo[i]!` returns an `α` or panics.
@@ -401,14 +400,14 @@ Those interested in theory and the intricate details may look there. I intend to
 Lean encodes errors as monads. The [`Option α`] type is by far the most used.
 
 An `Option α` is the following type:
-```lean
+```haskell
 inductive Option (α : Type) where
   | none
   | some (val : α)
 ```
 
 There are other forms of errors. The [`Except ε α`] type allows for encoding a specific error type:
-```lean
+```haskell
 inductive Except (ε : Type) (α : Type) where
   | error (err : ε)
   | ok (val : α)
@@ -424,7 +423,7 @@ Iteration is thus *useless* in the pure context! We can iterate, for sure, but t
 
 It should be noted that the `do` in `for/in/do` and `while/do` are part of their declaration syntax, and are unrelated to the `do` keyword. Morally, they're the same `do`, though.
 
-### implementing iterators: `ForIn` and `Stream`
+#### implementing iterators: `ForIn` and `Stream`
 
 `for` desugars to an appliction of the `ForIn.forIn` method, so that data structures can implement individually what exactly iteration means for them.
 
@@ -432,9 +431,9 @@ The iteration implemented by `ForIn` is called "internal iteration", which means
 
 One reason to prefer internal iteration is that it is easier to verify termination. This is something Lean cares very much about. But, internal iteration is a less flexible model than external iteration. You can't quite just convert an internal iterator to an external iterator. So there are some downsides.
 
-Lean also has an external iteration typeclass, called `Stream`, but it is not used as much. `Stream α` provides a `.next?` method that returns an `Option (α × Stream α)`: however, because Lean is purely functional, the burden is on the user to use this new `Stream α`.
+Lean also has an external iteration typeclass, called `Stream`, but it is not used as much. `Stream α` provides a `.next?` method that returns an `Option (α × Stream α)`. However, because Lean is purely functional, the burden is on the user to shadow bindings and use this new `Stream α`.
 
-It is perhaps possible to do external iteration via the State monad. I would like to try this out.
+It is probably possible to do external iteration via the State monad. I would like to try this out.
 
 ## Modules
 
@@ -442,7 +441,7 @@ It is perhaps possible to do external iteration via the State monad. I would lik
 
 The standard reference is [Metaprogramming in Lean](https://leanprover-community.github.io/lean4-metaprogramming-book/).
 
-I will make no attempt to describe Lean's system in detail: but I do plan to provide a high-level overview.
+I will make no attempt to describe Lean's system in detail. I do plan to provide a high-level overview.
 
 ## Proof