meow

1 files changed, 73 insertions, 36 deletions

diff --git a/plt/lean.md b/plt/lean.md
index 41bf622..695d45c 100644
--- a/plt/lean.md
+++ b/plt/lean.md
@@ -3,40 +3,46 @@ layout: plt
 title: An Unofficial Lean Reference
 ---
 
-# a lean 4 reference
+# imperative programming in lean
 
-Lean is a combination programming language and theorem prover. It's a pretty neat language!
+[Lean](https://lean-lang.org/) is a combination programming language and theorem prover. It's a pretty neat language!
+
+I found it hard to get started with, however. This guide is an attempt at remedying that.
 
 ## table of contents
 
-- Documentation
-- Core Lean
+- [Documentation](#documentation)
+- [Prelude](#prelude)
 - Evaluation
 - Assignment
 - Data Types
-  - `structure`
-  - `inductive`
-  - `class`
-  - `List` and `Array`
-  - `Nat`, `Fin`, and `USize`
-- Iteration
+  - Structural Types
+  - Inductive Types
+  - Booleans
+  - Numbers
+  - Lists
 - Classes
 - Coersion
-- Modules
+- Errors
+- [Iteration](#iteration)
+- IO
 - Monads
+- Modules
 - Macros
+- Proof
+  - Dependent Types
+  - Tactics
 
 ## Documentation
 
 First: where is the documentation?
 
-The primary source of documentation is the [Lean API docs](https://leanprover-community.github.io/mathlib4_docs/). Despite the URL, they cover more than just mathlib - also generating docs from the (heavily commented) standard library and compiler code base. Lean does not have a comprehensive reference manual, but these docs are as close as it gets.
+The primary source of documentation is the [Lean source code documentation](https://leanprover-community.github.io/mathlib4_docs/). Despite the URL, it covers more than just mathlib - also generating docs from the (heavily commented) standard library and compiler code base. Lean does not have a comprehensive reference manual, but these docs are as close as it gets.
 
-The secondary source of documentation is the [Lean Zulip](https://leanprover.zulipchat.com/). Zulip is a tool that is for chat software what Stack Exchange was for forums: it turns them into a searchable, indexable<sup>`[1]`</sup> *knowledge database*. The Lean Zulip in particular is host to a wide variety of wonderfully nice and extremely knowledgeable people: with both channels for compiler development and new-to-Lean questions alike.
+The secondary source of documentation is the [Lean Zulip](https://leanprover.zulipchat.com/). Zulip is a tool that is for chat software what Stack Exchange was for forums: it turns them into a searchable, <span title="Though, it doesn't seem to be indexed by Google.">indexable</span> *knowledge database*. The Lean Zulip in particular is host to a wide variety of wonderfully nice and very knowledgeable people: with both channels for compiler development and new-to-Lean questions alike.
 
 There is additionally the [official documentation page](https://lean-lang.org/documentation/) and the [unofficial documentation page](https://leanprover-community.github.io/learn.html), which together catalogue most all of the other learning resources available for Lean.
-
-There are several books written for Lean. Depending on what you want to do, [*Theorem Proving in Lean*](https://leanprover.github.io/theorem_proving_in_lean4/introduction.html) or [*Functional Programming in Lean*](https://leanprover.github.io/functional_programming_in_lean/introduction.html) are alternately recommended. There are also a good deal more, which I have not read:
+There are also several books written for Lean. Depending on what you want to do, [*Theorem Proving in Lean*](https://leanprover.github.io/theorem_proving_in_lean4/introduction.html) or [*Functional Programming in Lean*](https://leanprover.github.io/functional_programming_in_lean/introduction.html) are alternately recommended. There are a good deal more, which I have not read:
 - [*Mathematics in Lean*](https://leanprover-community.github.io/mathematics_in_lean/)
 - [*The Mechanics of Proof*](https://hrmacbeth.github.io/math2001/)
 - [*The Hitchhiker's Guide to Logical Verification*](https://browncs1951x.github.io/static/files/hitchhikersguide.pdf)
@@ -44,19 +50,15 @@ There are several books written for Lean. Depending on what you want to do, [*Th
 
 Finally, there is [the Lean manual](https://lean-lang.org/lean4/doc/). It is *very* much a work in progress, and contains plenty of blank pages: but, I've found some sections helpful on occasion.
 
-`[1]`: Though, it doesn't seem to be indexed by Google.
-
 ## Prelude
 
 Second: what is *in* the language, really? Is there a syntactic reference?
 
 The short answer is no, there is not a syntax reference, and if there existed one it wouldn't be very helpful. Lean has an extremely powerful metaprogramming system: and the majority of *syntax* in Lean is user-defined.
 
-The best way to find out what you're looking at is to use VS Code's right-click "Go to Declaration" feature. On a type, it'll drop you at its declaration. On a term, it'll drop you on its definition. On a *syntactic element*, it will either drop you into the core Lean codebase, or, more likely, onto a *macro syntax rule*. (If you are not writing Lean in VS Code, by the way, you should be. Lean has *extremely* good tooling that is primarily based around VS Code. Emacs is the only other option but is much less maintained.)
-
 However. To my best understanding, the syntactic forms are as follows:
 - types: `:`
-  - [`structure`] [`inductive`] `coinductive` [`class`] `instance`
+  - [`structure`] [`inductive`] <span title="Coinductive types do not actually exist yet.">`coinductive`</span> [`class`] `instance`
   - `where` `instance` `extends` `deriving`
 - values:
   - `""` `''` `«»` `[]` `#[]` `{}` `()` `fun` `λ`
@@ -98,18 +100,19 @@ This list is unlikely to be comprehensive.
 The standard data types included in core Lean are the following:
 - unit: [`Unit`]
 - booleans: [`Bool`]
-- numbers:
-  - [`Nat`], [`Int`], [`Fin n`]
-  - [`USize`], [`UInt8`], [`UInt16`], [`UInt32`], [`UInt64`], [`BitVec`]
-- strings: [`Char`], [`String`], [`Substring`]
-- lists: [`List α`], [`Array α`], [`Subarray`] (see also: [`Batteries.Vector α n`])
-  - [`ByteArray`], [`FloatArray`] (these may be optimized out in the future)
-- errors: [`Option α`], [`Except ε α`]
-- data: [`Prod α β`], [`Sum α β`] (see also: `structure`, `inductive`)
-- types: [`Empty`], [`Nonempty`], [`Type`/`Prop`/`Type u`/`Sort u`]
+- numbers: [`Nat`] [`Int`] [`Fin n`]
+  - [`USize`] [`UInt8`] [`UInt16`] [`UInt32`] [`UInt64`] [`BitVec`]
+- strings: [`Char`] [`String`] [`Substring`]
+- lists: [`List α`] [`Array α`] [`Subarray`]
+  - [`ByteArray`] [`FloatArray`]
+  - (see also: [`Batteries.Vector α n`])
+- errors: [`Option α`] [`Except ε α`]
+- data: [`Prod α β`] [`Sum α β`]
+  - (see also: `structure` `inductive`)
+- types: [`Empty`] [`Nonempty`] [`Type`/`Prop`/`Type u`/`Sort u`]
 - proof:
-  - [`And α β`], [`Or α β`], [`Iff α β`], [`True`], [`False`]
-  - [`Eq α β`], [`Equivalence`]
+  - [`And α β`] [`Or α β`] [`Iff α β`] [`True`] [`False`]
+  - [`Eq α β`] [`Equivalence`]
   - [`Exists`] (where is `Forall`?)
 
 [`Unit`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Unit
@@ -148,22 +151,56 @@ The standard data types included in core Lean are the following:
 [`Equivalence`]: https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Equivalence
 [`Exists`]: https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Exists
 
+The best way to find out what you're looking at is to use VS Code's right-click "Go to Declaration" feature. On a type, it'll drop you at its declaration. On a term, it'll drop you on its definition. On a *syntactic element*, it will either drop you into the core Lean codebase, or, more likely, onto a *macro syntax rule*.
+
+(If you are not writing Lean in VS Code, by the way, you should be. Lean has *extremely* good tooling that is primarily based around VS Code. Emacs is the only other option but is much less maintained.)
+
+## Evaluation
+
+## Assignment
+
+## Data Types
+
+### Structural Types
+
+### Inductive Types
+
+### Booleans
+
+### Numbers
+
+### Lists
+
+## Errors
+
 ## Iteration
 
 Lean has three main syntactic constructs for iteration: `for`, `while`, and `repeat`. They all function pretty much as you would expect and ultimately desugar to lambdas and (tail) recursion.
 
-However: Lean is a purely functional language, as much as it does a good job at hiding it. In the default (pure) context, variable mutation is not allowed. Neither is IO, nor any sort of side effects. And `for`/`while`/`repeat` <span title="Okay, okay, they return PUnit. You know what I meant :-P">do not return to a value<sup>*</sup>.</span>
+However: Lean is a purely functional language, as much as it does a good job at hiding it. In the default (pure) context, variable mutation is not allowed. Neither is IO, nor any sort of side effects. And `for`/`while`/`repeat` return only the Unit value, providing no information.
 
 Iteration is thus *useless* in the pure context! We can iterate, for sure, but there may never be any *observable* changes. As such, Lean does not allow `for`/`while`/`repeat` within pure functions. This can be the cause of some strange type errors. Ensure you are only iterating in a monadic `do` context.
 
-It should be noted that the `do` in `for <item> in <iter> do` and `while <cond> do` are part of the `for`/`while` declaration syntax, and are unrelated to the `do` keyword. Morally, they're the same `do`, though.
+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`
 
 `for` desugars to an appliction of the `ForIn.forIn` method, so that data structures can implement individually what exactly iteration means for them.
 
-The iteration implemented by `ForIn` is called "internal iteration", which means it is a higher order function where you give the body of the loop to it to run on the elements yielded by the iterator in order. This is in contrast to "external iteration" (in the style of Rust), where the iterator has a function returning the next value of the iterator.
-
-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 (value × stream)`
+The iteration implemented by `ForIn` is called "internal iteration", which means it is a higher order function where you give the body of the loop to it to run on the elements yielded by the iterator in order. This is in contrast to "external iteration" (in the style of ex. Rust), where the iterator has a function returning the next value of the iterator.
 
 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 α`.
+
+It is perhaps possible to do external iteration via the State monad. I would like to try this out.
+
+## IO
+
+## Monads
+
+## Modules
+
+## Macros
+
+## Proof