diff --git a/.vscode/settings.json b/.vscode/settings.json
index 86f8a589b6..7f92a670e2 100644
--- a/.vscode/settings.json
+++ b/.vscode/settings.json
@@ -1,4 +1,7 @@
 {
     "files.insertFinalNewline": true,
-    "files.trimTrailingWhitespace": true
+    "files.trimTrailingWhitespace": true,
+    "[markdown]": {
+        "rewrap.wrappingColumn": 70
+    }
 }
diff --git a/doc/bool.md b/doc/bool.md
new file mode 100644
index 0000000000..88963b5e90
--- /dev/null
+++ b/doc/bool.md
@@ -0,0 +1 @@
+# Booleans
diff --git a/doc/declarations.md b/doc/declarations.md
index 787b78acaf..2b9752ed9d 100644
--- a/doc/declarations.md
+++ b/doc/declarations.md
@@ -5,7 +5,7 @@
 Declaration Names
 =================
 
-A declaration name is a :ref:`hierarchical identifier <identifiers>` that is interpreted relative to the current namespace as well as (during lookup) to the set of open namespaces.
+A declaration name is a hierarchical [identifier](lexical_structure.md#identifiers) that is interpreted relative to the current namespace as well as (during lookup) to the set of open namespaces.
 
 .. code-block:: lean
 
@@ -34,15 +34,15 @@ Contexts and Telescopes
 
 When processing user input, Lean first parses text to a raw expression format. It then uses background information and type constants to disambiguate overloaded symbols and infer implicit arguments, resulting in a fully-formed expression. This process is known as *elaboration*.
 
-As hinted in :numref:`expression_syntax`, expressions are parsed and
-elaborated with respect to an *environment* and a *local
-context*. Roughly speaking, an environment represents the state of
-Lean at the point where an expression is parsed, including previously
-declared axioms, constants, definitions, and theorems. In a given
-environment, a *local context* consists of a sequence ``(a₁ : α₁)
-(a₂ : α₂) ... (aₙ : αₙ)`` where each ``aᵢ`` is a name denoting a local
-constant and each ``αᵢ`` is an expression of type ``Sort u`` for some
-``u`` which can involve elements of the environment and the local
+As hinted in [Expression Syntax](expressions.md#expression_syntax),
+expressions are parsed and elaborated with respect to an *environment*
+and a *local context*. Roughly speaking, an environment represents the
+state of Lean at the point where an expression is parsed, including
+previously declared axioms, constants, definitions, and theorems. In a
+given environment, a *local context* consists of a sequence ``(a₁ :
+α₁) (a₂ : α₂) ... (aₙ : αₙ)`` where each ``aᵢ`` is a name denoting a
+local constant and each ``αᵢ`` is an expression of type ``Sort u`` for
+some ``u`` which can involve elements of the environment and the local
 constants ``aⱼ`` for ``j < i``.
 
 Intuitively, a local context is a list of variables that are held constant while an expression is being elaborated. Consider the following
@@ -62,7 +62,7 @@ Here ``a b c : Nat`` indicates the local context, and the second ``Nat`` indicat
 
 A *context* is sometimes called a *telescope*, but the latter is used more generally to include a sequence of declarations occuring relative to a given context. For example, relative to the context ``(a₁ : α₁) (a₂ : α₂) ... (aₙ : αₙ)``, the types ``βᵢ`` in a telescope ``(b₁ : β₁) (b₂ : β₂) ... (bₙ : βₙ)`` can refer to ``a₁, ..., aₙ``. Thus a context can be viewed as a telescope relative to the empty context.
 
-Telescopes are often used to describe a list of arguments, or parameters, to a declaration. In such cases, it is often notationally convenient to let ``(a : α)`` stand for a telescope rather than just a single argument. In general, the annotations described in :ref:`implicit_arguments` can be used to mark arguments as implicit.
+Telescopes are often used to describe a list of arguments, or parameters, to a declaration. In such cases, it is often notationally convenient to let ``(a : α)`` stand for a telescope rather than just a single argument. In general, the annotations described in [Implicit Arguments](expressions.md#implicit_arguments) can be used to mark arguments as implicit.
 
 .. _basic_declarations:
 
@@ -228,7 +228,7 @@ Below are some common examples of inductive types, many of which are defined in
 
 Note that in the syntax of the inductive definition ``foo``, the context ``(a : α)`` is left implicit. In other words, constructors and recursive arguments are written as though they have return type ``foo`` rather than ``foo a``.
 
-Elements of the context ``(a : α)`` can be marked implicit as described in :numref:`implicit_arguments`. These annotations bear only on the type former, ``foo``. Lean uses a heuristic to determine which arguments to the constructors should be marked implicit, namely, an argument is marked implicit if it can be inferred from the type of a subsequent argument. If the annotation ``{}`` appears after the constructor, a argument is marked implicit if it can be inferred from the type of a subsequent argument *or the return type*. For example, it is useful to let ``nil`` denote the empty list of any type, since the type can usually be inferred in the context in which it appears. These heuristics are imperfect, and you may sometimes wish to define your own constructors in terms of the default ones. In that case, use the ``[pattern]`` :ref:`attribute <attributes>` to ensure that these will be used appropriately by the :ref:`equation compiler <the_equation_compiler>`.
+Elements of the context ``(a : α)`` can be marked implicit as described in [Implicit Arguments](#implicit.md#implicit_arguments). These annotations bear only on the type former, ``foo``. Lean uses a heuristic to determine which arguments to the constructors should be marked implicit, namely, an argument is marked implicit if it can be inferred from the type of a subsequent argument. If the annotation ``{}`` appears after the constructor, a argument is marked implicit if it can be inferred from the type of a subsequent argument *or the return type*. For example, it is useful to let ``nil`` denote the empty list of any type, since the type can usually be inferred in the context in which it appears. These heuristics are imperfect, and you may sometimes wish to define your own constructors in terms of the default ones. In that case, use the ``[pattern]`` [attribute](TODO: missing link) to ensure that these will be used appropriately by the [Equation Compiler](#the-equation-compiler).
 
 There are restrictions on the universe ``u`` in the return type ``Sort u`` of the type former. There are also restrictions on the universe ``u`` in the return type ``Sort u`` of the motive of the eliminator. These will be discussed in the next section in the more general setting of inductive families.
 
@@ -270,7 +270,7 @@ The type former, constructors, and eliminator are all part of Lean's axiomatic f
 - ``foo.below``, ``foo.ibelow`` : functions used by the equation compiler to implement structural recursion
 - ``foo.sizeof`` : a measure which can be used for well-founded recursion
 
-Note that it is common to put definitions and theorems related to a datatype ``foo`` in a namespace of the same name. This makes it possible to use projection notation described in :numref:`structures_and_records` and :numref:`namespaces`.
+Note that it is common to put definitions and theorems related to a datatype ``foo`` in a namespace of the same name. This makes it possible to use projection notation described in [Structures](struct.md#structures) and [Namespaces](namespaces.md#namespaces).
 
 .. code-block:: lean
 
@@ -450,7 +450,7 @@ Each ``patternsᵢ`` is a sequence of patterns of the same length as ``(b : β)`
 
 In the last case, the pattern must be enclosed in parentheses.
 
-Each term ``tᵢ`` is an expression in the context ``(a : α)`` together with the variables introduced on the left-hand side of the token ``:=``. The term ``tᵢ`` can also include recursive calls to ``foo``, as described below. The equation compiler does case splitting on the variables ``(b : β)`` as necessary to match the patterns, and defines ``foo`` so that it has the value ``tᵢ`` in each of the cases. In ideal circumstances (see below), the equations hold definitionally. Whether they hold definitionally or only propositionally, the equation compiler proves the relevant equations and assigns them internal names. They are accessible by the ``rewrite`` and ``simp`` tactics under the name ``foo`` (see :numref:`the_rewriter` and :numref:`the_simplifier`). If some of the patterns overlap, the equation compiler interprets the definition so that the first matching pattern applies in each case. Thus, if the last pattern is a variable, it covers all the remaining cases. If the patterns that are presented do not cover all possible cases, the equation compiler raises an error.
+Each term ``tᵢ`` is an expression in the context ``(a : α)`` together with the variables introduced on the left-hand side of the token ``:=``. The term ``tᵢ`` can also include recursive calls to ``foo``, as described below. The equation compiler does case splitting on the variables ``(b : β)`` as necessary to match the patterns, and defines ``foo`` so that it has the value ``tᵢ`` in each of the cases. In ideal circumstances (see below), the equations hold definitionally. Whether they hold definitionally or only propositionally, the equation compiler proves the relevant equations and assigns them internal names. They are accessible by the ``rewrite`` and ``simp`` tactics under the name ``foo`` (see [Rewrite](tactics.md#rewrite) and _[TODO: where is simplifier tactic documented?]_. If some of the patterns overlap, the equation compiler interprets the definition so that the first matching pattern applies in each case. Thus, if the last pattern is a variable, it covers all the remaining cases. If the patterns that are presented do not cover all possible cases, the equation compiler raises an error.
 
 When identifiers are marked with the ``[pattern]`` attribute, the equation compiler unfolds them in the hopes of exposing a constructor. For example, this makes it possible to write ``n+1`` and ``0`` instead of ``nat.succ n`` and ``nat.zero`` in patterns.
 
@@ -525,7 +525,7 @@ If structural recursion fails, the equation compiler falls back on well-founded
 
 Note that recursive definitions can in general require nested recursions, that is, recursion on different arguments of ``foo`` in the template above. The equation compiler handles this by abstracting later arguments, and recursively defining higher-order functions to meet the specification.
 
-The equation compiler also allows mutual recursive definitions, with a syntax similar to that of :ref:`mutual inductive definitions <mutual_and_nested_inductive_definitions>`. They are compiled using well-founded recursion, and so once again the defining equations hold only propositionally.
+The equation compiler also allows mutual recursive definitions, with a syntax similar to that of [Mutual and Nested Inductive Definitions](#mutual-and-nested-inductive-definitions). They are compiled using well-founded recursion, and so once again the defining equations hold only propositionally.
 
 .. code-block:: lean
 
@@ -543,7 +543,7 @@ The equation compiler also allows mutual recursive definitions, with a syntax si
     example (a : Nat) : odd (a + 1) = even a :=
     by simp [odd]
 
-Well-founded recursion is especially useful with :ref:`mutual and nested inductive definitions <mutual_and_nested_inductive_definitions>`, since it provides the canonical way of defining functions on these types.
+Well-founded recursion is especially useful with [Mutual and Nested Inductive Definitions](#mutual-and-nested-inductive-definitions), since it provides the canonical way of defining functions on these types.
 
 .. code-block:: lean
 
@@ -647,7 +647,7 @@ Lean supports a ``match ... with ...`` construct similar to ones found in most f
 
 Here ``t₁, ..., tₙ`` are any terms in the context in which the expression appears, the expressions ``pᵢⱼ`` are patterns, and the terms ``sᵢ`` are expressions in the local context together with variables introduced by the patterns on the left-hand side. Each ``sᵢ`` should have the expected type of the entire ``match`` expression.
 
-Any ``match`` expression is interpreted using the equation compiler, which generalizes ``t₁, ..., tₙ``, defines an internal function meeting the specification, and then applies it to ``t₁, ..., tₙ``. In contrast to the definitions in :numref:`the_equation_compiler`, the terms ``tᵢ`` are arbitrary terms rather than just variables, and the expression can occur anywhere within a Lean expression, not just at the top level of a definition. Note that the syntax here is somewhat different: both the terms ``tᵢ`` and the patterns ``pᵢⱼ`` are separated by commas.
+Any ``match`` expression is interpreted using the equation compiler, which generalizes ``t₁, ..., tₙ``, defines an internal function meeting the specification, and then applies it to ``t₁, ..., tₙ``. In contrast to the definitions in [The Equation Compiler](declarations.md#the-equation-compiler), the terms ``tᵢ`` are arbitrary terms rather than just variables, and the expression can occur anywhere within a Lean expression, not just at the top level of a definition. Note that the syntax here is somewhat different: both the terms ``tᵢ`` and the patterns ``pᵢⱼ`` are separated by commas.
 
 .. code-block:: lean
 
@@ -712,7 +712,7 @@ Given ``c : foo``, Lean offers the following convenient syntax for the projectio
 - *anonymous projections* : ``c.fieldᵢ``
 - *numbered projections* : ``c.i``
 
-These can be used in any situation where Lean can infer that the type of ``c`` is of the form ``foo a``. The convention for anonymous projections is extended to any function ``f`` defined in the namespace ``foo``, as described in :numref:`namespaces`.
+These can be used in any situation where Lean can infer that the type of ``c`` is of the form ``foo a``. The convention for anonymous projections is extended to any function ``f`` defined in the namespace ``foo``, as described in [Namespaces](namespaces.md).
 
 Similarly, Lean offers the following convenient syntax for constructing elements of ``foo``. They are equivalent to ``foo.constructor b₁ b₂ f₁ f₁ ... fₙ``, where ``b₁ : foo``, ``b₂ : bar``, and each ``fᵢ : βᵢ`` :
 
diff --git a/doc/dev/index.md b/doc/dev/index.md
index 7a8dc48d16..0496704149 100644
--- a/doc/dev/index.md
+++ b/doc/dev/index.md
@@ -36,13 +36,21 @@ go-to-definition in the stdlib (automatically set when using
 
 You can use [`elan`](https://github.com/leanprover/elan) to easily
 switch between stages and build configurations based on the current
-directory, both for the `lean/leanc/leanmake` binaries in your shell's
+directory, both for the `lean`, `leanc`, and `leanmake` binaries in your shell's
 PATH and inside your editor.
 
 To install elan, you can do so, without installing a default version of Lean, using
+
 ```bash
+[Unix]
 curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none
+
+[Windows]
+curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1
+powershell -f elan-init.ps1 --default-toolchain none
+del elan-init.ps1
 ```
+
 You can use `elan toolchain link` to give a specific stage build
 directory a reference name, then use `elan override set` to associate
 such a name to the current directory. We usually want to use `stage0`
diff --git a/doc/dev/mdbook.md b/doc/dev/mdbook.md
index a80975cca6..7e8f00e27c 100644
--- a/doc/dev/mdbook.md
+++ b/doc/dev/mdbook.md
@@ -1,7 +1,26 @@
-This manual is generated by [mdBook](https://github.com/rust-lang/mdBook). We are currently using a
-[fork](https://github.com/leanprover/mdBook) of it for the following additional features:
+## Settings
 
-* Add support for hiding lines in other languages [#1339](https://github.com/rust-lang/mdBook/pull/1339)
+We are using the following settings while editing the markdown docs.
+
+```json
+{
+    "files.insertFinalNewline": true,
+    "files.trimTrailingWhitespace": true,
+    "[markdown]": {
+        "rewrap.wrappingColumn": 70
+    }
+}
+```
+
+## Build
+
+This manual is generated by
+[mdBook](https://github.com/rust-lang/mdBook). We are currently using
+a [fork](https://github.com/leanprover/mdBook) of it for the following
+additional features:
+
+* Add support for hiding lines in other languages
+  [#1339](https://github.com/rust-lang/mdBook/pull/1339)
 * Replace calling `rustdoc --test` from `mdbook test` with `./test`
 
 To build this manual, first install the fork via
@@ -9,6 +28,7 @@ To build this manual, first install the fork via
 cargo install --git https://github.com/leanprover/mdBook mdbook
 ```
 Then use e.g. [`mdbook watch`](https://rust-lang.github.io/mdBook/cli/watch.html) in the `doc/` folder:
+
 ```bash
 cd doc
 mdbook watch --open  # opens the output in `out/` in your default browser
@@ -16,7 +36,8 @@ mdbook watch --open  # opens the output in `out/` in your default browser
 
 Run `mdbook test` to test all `lean` code blocks.
 
-Using the [Nix setup](make/nix.md), you can instead open a shell with the mdBook fork downloaded from our binary cache:
+Using the [Nix setup](make/nix.md), you can instead open a shell with
+the mdBook fork downloaded from our binary cache:
 ```bash
 nix develop .#doc
 ```
diff --git a/doc/expressions.md b/doc/expressions.md
index 5e2a787d49..7fdf8880d3 100644
--- a/doc/expressions.md
+++ b/doc/expressions.md
@@ -1,37 +1,11 @@
 Expressions
 ===========
 
+Every expression in Lean has a [Type](types.md). Every type is also an
+expression of type `Sort u` for some universe level u. See [Type
+Universes](types.md#type_universes).
 
-<a name="_universes.md"></a>Universes
-=========
-
-Every type in Lean is, by definition, an expression of type ``Sort u``
-for some universe level ``u``. A universe level is one of the
-following:
-
-* a natural number, ``n``
-* a universe variable, ``u`` (declared with the command ``universe`` or ``universes``)
-* an expression ``u + n``, where ``u`` is a universe level and ``n`` is a natural number
-* an expression ``max u v``, where ``u`` and ``v`` are universes
-* an expression ``imax u v``, where ``u`` and ``v`` are universe levels
-
-The last one denotes the universe level ``0`` if ``v`` is ``0``, and ``max u v`` otherwise.
-
-```lean
-universe u v
-
-#check Sort u
-#check Sort 5
-#check Sort (u + 1)
-#check Sort (u + 3)
-#check Sort (max u v)
-#check Sort (max (u + 3) v)
-#check Sort (imax (u + 3) v)
-#check Prop
-#check Type
-```
-
-<a name="_expression_syntax"></a>Expression Syntax
+Expression Syntax
 =================
 
 The set of expressions in Lean is defined inductively as follows:
@@ -121,13 +95,13 @@ universe u
 #check (fun x => x) true
 ```
 
-<a name="_implicit_arguments"></a>Implicit Arguments
+Implicit Arguments
 ==================
 
 When declaring arguments to defined objects in Lean (for example, with
 ``def``, ``theorem``, ``axiom``, ``constant``, ``inductive``, or
 ``structure``; see [Chapter Declarations](./declarations.md) or when
-declaring variables in sections (see [Chapter Other Commands](./other_commands.md)),
+declaring variables in sections (see [Other Commands](./other_commands.md)),
 arguments can be annotated as *explicit* or *implicit*.
 This determines how expressions containing the object are interpreted.
 
@@ -289,15 +263,15 @@ def unbounded (f : Nat → Nat) : Prop := ∀ M, ∃ n, f n ≥ M
 Constructors, Projections, and Matching
 =======================================
 
-Lean's foundation, the *Calculus of Inductive Constructions*, supports the declaration of *inductive types*. Such types can have any number of *constructors*, and an associated *eliminator* (or *recursor*). Inductive types with one constructor, known as *structures*, have *projections*. The full syntax of inductive types is described in :numref:`Chapter %s <declarations>`, but here we describe some syntactic elements that facilitate their use in expressions.
+Lean's foundation, the *Calculus of Inductive Constructions*, supports the declaration of *inductive types*. Such types can have any number of *constructors*, and an associated *eliminator* (or *recursor*). Inductive types with one constructor, known as *structures*, have *projections*. The full syntax of inductive types is described in [Declarations](declarations.md), but here we describe some syntactic elements that facilitate their use in expressions.
 
 When Lean can infer the type of an expression and it is an inductive type with one constructor, then one can write ``⟨a1, a2, ..., an⟩`` to apply the constructor without naming it. For example, ``⟨a, b⟩`` denotes ``prod.mk a b`` in a context where the expression can be inferred to be a pair, and ``⟨h₁, h₂⟩`` denotes ``and.intro h₁ h₂`` in a context when the expression can be inferred to be a conjunction. The notation will nest constructions automatically, so ``⟨a1, a2, a3⟩`` is interpreted as ``prod.mk a1 (prod.mk a2 a3)`` when the expression is expected to have a type of the form ``α1 × α2 × α3``. (The latter is interpreted as ``α1 × (α2 × α3)``, since the product associates to the right.)
 
 Similarly, one can use "dot notation" for projections: one can write ``p.fst`` and ``p.snd`` for ``prod.fst p`` and ``prod.snd p`` when Lean can infer that ``p`` is an element of a product, and ``h.left`` and ``h.right`` for ``and.left h`` and ``and.right h`` when ``h`` is a conjunction.
 
-The anonymous projector notation can used more generally for any objects defined in a *namespace* (see :numref:`Chapter %s <other_commands>`). For example, if ``l`` has type ``list α`` then ``l.map f`` abbreviates ``list.map f l``, in which ``l`` has been placed at the first argument position where ``list.map`` expects a ``list``.
+The anonymous projector notation can used more generally for any objects defined in a *namespace* (see [Other Commands](other_commands.md)). For example, if ``l`` has type ``list α`` then ``l.map f`` abbreviates ``list.map f l``, in which ``l`` has been placed at the first argument position where ``list.map`` expects a ``list``.
 
-Finally, for data types with one constructor, one destruct an element by pattern matching using the ``let`` and ``assume`` constructs, as in the examples below. Internally, these are interpreted using the ``match`` construct, which is in turn compiled down for the eliminator for the inductive type, as described in :numref:`Chapter %s <declarations>`.
+Finally, for data types with one constructor, one destruct an element by pattern matching using the ``let`` and ``assume`` constructs, as in the examples below. Internally, these are interpreted using the ``match`` construct, which is in turn compiled down for the eliminator for the inductive type, as described in [Declarations](declarations.md).
 
 .. code-block:: lean
 
@@ -337,7 +311,7 @@ Finally, for data types with one constructor, one destruct an element by pattern
     theorem swap_conj'' {a b : Prop} : a ∧ b → b ∧ a :=
     assume ⟨ha, hb⟩, ⟨hb, ha⟩
 
-<a name="_structured_proofs"></a>Structured Proofs
+Structured Proofs
 =================
 
 Syntactic sugar is provided for writing structured proof terms:
@@ -423,7 +397,7 @@ Every expression in Lean has a natural computational interpretation, unless it i
 * *β-reduction* : An expression ``(λ x, t) s`` β-reduces to ``t[s/x]``, that is, the result of replacing ``x`` by ``s`` in ``t``.
 * *ζ-reduction* : An expression ``let x := s in t`` ζ-reduces to ``t[s/x]``.
 * *δ-reduction* : If ``c`` is a defined constant with definition ``t``, then ``c`` δ-reduces to to ``t``.
-* *ι-reduction* : When a function defined by recursion on an inductive type is applied to an element given by an explicit constructor, the result ι-reduces to the specified function value, as described in :numref:`inductive_types`.
+* *ι-reduction* : When a function defined by recursion on an inductive type is applied to an element given by an explicit constructor, the result ι-reduces to the specified function value, as described in [Inductive Types](inductive.md).
 
 The reduction relation is transitive, which is to say, is ``s`` reduces to ``s'`` and ``t`` reduces to ``t'``, then ``s t`` reduces to ``s' t'``, ``λ x, s`` reduces to ``λ x, s'``, and so on. If ``s`` and ``t`` reduce to a common term, they are said to be *definitionally equal*. Definitional equality is defined to be the smallest equivalence relation that satisfies all these properties and also includes α-equivalence and the following two relations:
 
@@ -474,7 +448,7 @@ Every computable definition in Lean is compiled to bytecode at definition time.
     example : (λ x, f x) = f := rfl
     example (p : Prop) (h₁ h₂ : p) : h₁ = h₂ := rfl
 
-Note: the combination of proof irrelevance and singleton ``Prop`` elimination in ι-reduction renders the ideal version of definitional equality, as described above, undecidable. Lean's procedure for checking definitional equality is only an approximation to the ideal. It is not transitive, as illustrated by the example below. Once again, this does not compromise the consistency or soundness of Lean; it only means that Lean is more conservative in the terms it recognizes as well typed, and this does not cause problems in practice. Singleton elimination will be discussed in greater detail in :numref:`inductive_types`.
+Note: the combination of proof irrelevance and singleton ``Prop`` elimination in ι-reduction renders the ideal version of definitional equality, as described above, undecidable. Lean's procedure for checking definitional equality is only an approximation to the ideal. It is not transitive, as illustrated by the example below. Once again, this does not compromise the consistency or soundness of Lean; it only means that Lean is more conservative in the terms it recognizes as well typed, and this does not cause problems in practice. Singleton elimination will be discussed in greater detail in [Inductive Types](inductive.md).
 
 .. code-block:: lean
 
@@ -493,7 +467,8 @@ Lean's foundational framework consists of:
 
 - type universes and dependent function types, as described above
 
-- inductive definitions, as described in :numref:`inductive_types` and :numref:`inductive_families`.
+- inductive definitions, as described in [Inductive Types](inductive.md) and
+[Inductive Families](declarations.md#inductive-families).
 
 In addition, the core library defines (and trusts) the following axiomatic extensions:
 
@@ -574,4 +549,4 @@ In addition, the core library defines (and trusts) the following axiomatic exten
 
 The quotient construction implies function extensionality. The ``choice`` principle, in conjunction with the others, makes the axiomatic foundation classical; in particular, it implies the law of the excluded middle and propositional decidability. Functions that make use of ``choice`` to produce data are incompatible with a computational interpretation, and do not produce bytecode. They have to be declared ``noncomputable``.
 
-For metaprogramming purposes, Lean also allows the definition of objects which stand outside the object language. These are denoted with the ``meta`` keyword, as described in :numref:`Chapter %s <programming>`.
+For metaprogramming purposes, Lean also allows the definition of objects which stand outside the object language. These are denoted with the ``meta`` keyword, as described in [Metaprogramming](metaprogramming.md).
diff --git a/doc/lexical_structure.md b/doc/lexical_structure.md
index ad98c0f3c0..3b62d226bd 100644
--- a/doc/lexical_structure.md
+++ b/doc/lexical_structure.md
@@ -2,17 +2,14 @@ Lexical Structure
 =================
 
 This section describes the detailed lexical structure of the Lean
-language. Many readers will want to skip this section on a first
-reading.
+language.
 
-Lean input is processed into a stream of tokens by its scanner, using
-the UTF-8 encoding. The next token is the longest matching prefix of
-the remaining input.
+A Lean program consists of a stream of UTF-8 tokens where each token
+is one of the following:
 
 ```
-   token: `symbol` | `command` | `ident` | `string` | `char` | `numeral` |
-        : `decimal` | `quoted_symbol` | `doc_comment` | `mod_doc_comment` |
-        : `field_notation`
+   token: symbol | command | ident | string | char | numeral |
+        : decimal | doc_comment | mod_doc_comment | field_notation
 ```
 
 Tokens can be separated by the whitespace characters space, tab, line
@@ -26,18 +23,17 @@ Symbols and Commands
 .. *(TODO: list built-in symbols and command tokens?)*
 
 Symbols are static tokens that are used in term notations and
-commands. They can be both keyword-like (e.g. the :keyword:`have
+commands. They can be both keyword-like (e.g. the `have
 <structured_proofs>` keyword) or use arbitrary Unicode characters.
 
 Command tokens are static tokens that prefix any top-level declaration
 or action. They are usually keyword-like, with transitory commands
-like :keyword:`#print <instructions>` prefixed by an additional
-``#``. The set of built-in commands is listed in the :numref:`Chapter
-%s <other_commands>` section.
+like `#print <instructions>` prefixed by the ``#`` character. The set
+of built-in commands is listed in [Other Commands](./other_commands.md).
 
 Users can dynamically extend the sets of both symbols (via the
-commands listed in :numref:`quoted_symbols`) and command tokens (via
-the :keyword:`[user_command] <attributes>` attribute).
+commands listed in [Quoted Symbols](#quoted-symbols) and command
+tokens (via the `[user_command] <attributes>` attribute).
 
 .. _identifiers:
 
@@ -56,28 +52,41 @@ Parts of atomic names can be escaped by enclosing them in pairs of French double
 ```
 
 ```
-   ident: `atomic_ident` | `ident` "." `atomic_ident`
-   atomic_ident: `atomic_ident_start` `atomic_ident_rest`*
-   atomic_ident_start: `letterlike` | "_" | `escaped_ident_part`
-   letterlike: [a-zA-Z] | `greek` | `coptic` | `letterlike_symbols`
+   ident: atomic_ident | ident "." atomic_ident
+   atomic_ident: atomic_ident_start atomic_ident_rest*
+   atomic_ident_start: letterlike | "_" | escaped_ident_part
+   letterlike: [a-zA-Z] | greek | coptic | letterlike_symbols
    greek: <[α-ωΑ-Ωἀ-῾] except for [λΠΣ]>
    coptic: [ϊ-ϻ]
    letterlike_symbols: [℀-⅏]
    escaped_ident_part: "«" [^«»\r\n\t]* "»"
-   atomic_ident_rest: `atomic_ident_start` | [0-9'ⁿ] | `subscript`
+   atomic_ident_rest: atomic_ident_start | [0-9'ⁿ] | subscript
    subscript: [₀-₉ₐ-ₜᵢ-ᵪ]
 ```
 
 String Literals
 ===============
 
-String literals are enclosed by double quotes (``"``). They may contain line breaks, which are conserved in the string value.
+String literals are enclosed by double quotes (``"``). They may contain line breaks, which are conserved in the string value.  Backslash (`\`) is a special escape character which can be used to the following
+special characters:
+- `\\` represents an escaped backslash, so this escape causes one backslash to be included in the string.
+- `\"` puts a double quote in the string.
+- `\'` puts an apostrophe in the string.
+- `\n` puts a new line character in the string.
+- `\t` puts a tab character in the string.
+- `\xHH` puts the character represented by the 2 digit hexadecimal into the string.  For example
+"this \x26 that" which become "this & that".  Values above 0x80 will be interpreted according to the
+[Unicode table](https://unicode-table.com/en/) so "\xA9 Copyright 2021" is "© Copyright 2021".
+- `\uHHHH` puts the character represented by the 4 digit hexadecimal into the string, so the following
+string "\u65e5\u672c" will become "日本" which means "Japan".
+
+So the complete syntax is:
 
 ```
-   string       : '"' `string_item` '"'
-   string_item  : `string_char` | `string_escape`
+   string       : '"' string_item '"'
+   string_item  : string_char | string_escape
    string_char  : [^\\]
-   string_escape: "\" ("\" | '"' | "'" | "n" | "t" | "x" `hex_char` `hex_char`)
+   string_escape: "\" ("\" | '"' | "'" | "n" | "t" | "x" hex_char{2} | "u" hex_char{4} )
    hex_char     : [0-9a-fA-F]
 ```
 
@@ -87,7 +96,7 @@ Char Literals
 Char literals are enclosed by single quotes (``'``).
 
 ```
-   char: "'" `string_item` "'"
+   char: "'" string_item "'"
 ```
 
 Numeric Literals
@@ -96,43 +105,33 @@ Numeric Literals
 Numeric literals can be specified in various bases.
 
 ```
-   numeral    : `numeral10` | `numeral2` | `numeral8` | `numeral16`
+   numeral    : numeral10 | numeral2 | numeral8 | numeral16
    numeral10  : [0-9]+
    numeral2   : "0" [bB] [0-1]+
    numeral8   : "0" [oO] [0-7]+
-   numeral16  : "0" [xX] `hex_char`+
+   numeral16  : "0" [xX] hex_char+
 ```
 
-Decimal literals are currently only being used for some :keyword:`set_option <options>` values.
-
+Floating point literals are also possible with optional exponent:
 
 ```
-   decimal    : [0-9]+ "." [0-9]+
+   float    : [0-9]+ "." [0-9]+ [[eE[+-][0-9]+]
 ```
 
-Quoted Symbols
-==============
-
-In a fixed set of commands (:keyword:`notation
-<notation_declarations>`, :keyword:`local notation
-<notation_declarations>`, and :keyword:`reserve
-<notation_declarations>`), symbols (known or unknown) can be quoted by
-enclosing them in backticks (`````). Quoted symbols are used by these
-commands for registering new notations and symbols.
+For example:
 
 ```
-   quoted_symbol      : "`" " "* `quoted_symbol_start` `quoted_symbol_rest`* " "* "`"
-   quoted_symbol_start: [^0-9"\n\t `]
-   quoted_symbol_rest : [^"\n\t `]
+constant w : Int := 55
+constant x : Nat := 26085
+constant y : Nat := 0x65E5
+constant z : Float := 2.548123e-05
 ```
 
-A quoted symbol may contain surrounding whitespace, which is
-customarily used for pretty printing the symbol and ignored while
-scanning.
+Note: that negative numbers are created by applying the "-" negation prefix operator to the number, for example:
 
-While backticks are not allowed in a user-defined symbol, they are
-used in some built-in symbols (see :ref:`quotations`), which are
-accessible outside of the set of commands noted above.
+```
+constant w : Int := -55
+```
 
 Doc Comments
 ============
@@ -150,9 +149,9 @@ Field Notation
 
 Trailing field notation tokens are used in expressions such as
 ``(1+1).to_string``. Note that ``a.toString`` is a single
-:ref:`identifier <identifiers>`, but may be interpreted as a field
+[Identifier](#identifiers), but may be interpreted as a field
 notation expression by the parser.
 
 ```
-   field_notation: "." ([0-9]+ | `atomic_ident`)
+   field_notation: "." ([0-9]+ | atomic_ident)
 ```
diff --git a/doc/other_commands.md b/doc/other_commands.md
new file mode 100644
index 0000000000..09f25de218
--- /dev/null
+++ b/doc/other_commands.md
@@ -0,0 +1 @@
+# Other Commands
\ No newline at end of file
diff --git a/doc/quickstart.md b/doc/quickstart.md
index 4b19bcaeea..8cb1b4ac9b 100644
--- a/doc/quickstart.md
+++ b/doc/quickstart.md
@@ -9,7 +9,7 @@ See [Setup](./setup.md) for other ways and more details on setting up Lean.
     ```
     Alternatively, on Windows, download [the latest release](https://github.com/leanprover/elan/releases/latest/download/elan-x86_64-pc-windows-msvc.zip) and run the contained `elan-init.exe`.
     See the [elan repo](https://github.com/leanprover/elan) for other installation options and details.
-
+    
 1. Install [VS Code](https://code.visualstudio.com/).
 
 1. Open VS Code and install the `lean4` extension.
diff --git a/doc/syntax.md b/doc/syntax.md
index a9f1632409..af0100a94f 100644
--- a/doc/syntax.md
+++ b/doc/syntax.md
@@ -1,16 +1,27 @@
 # Syntax Extensions
 
-Lean's syntax can be extended and customized by users at every level, ranging from basic "mixfix" notations to custom elaborators.
-In fact, all builtin syntax is parsed and processed using the same mechanisms and APIs open to users.
-In this section, we will describe and explain the various extension points.
-Significant syntax extensions already builtin into Lean such as the [`do` notation](./do.md) are described in subsections.
+[Lean's syntax](lexical_structure.md) can be extended and customized
+by users at every level, ranging from basic "mixfix" notations to
+custom elaborators. In fact, all builtin syntax is parsed and
+processed using the same mechanisms and APIs open to users. In this
+section, we will describe and explain the various extension points.
+Significant syntax extensions already builtin into Lean such as the
+[`do` notation](./do.md) are described in subsections.
 
-While introducing new notations is a relatively rare feature in programming languages and sometimes even frowned upon because of its potential to obscure code, it is an invaluable tool in formalization for expressing established conventions and notations of the respective field succinctly in code.
-Going beyond basic notations, Lean's ability to factor out common boilerplate code into (well-behaved) macros and to embed entire custom domain specific languages (DSLs) to textually encode subproblems efficiently and readably can be of great benefit to both programmers and proof engineers alike.
+While introducing new notations is a relatively rare feature in
+programming languages and sometimes even frowned upon because of its
+potential to obscure code, it is an invaluable tool in formalization
+for expressing established conventions and notations of the respective
+field succinctly in code. Going beyond basic notations, Lean's ability
+to factor out common boilerplate code into (well-behaved) macros and
+to embed entire custom domain specific languages (DSLs) to textually
+encode subproblems efficiently and readably can be of great benefit to
+both programmers and proof engineers alike.
 
 ## Notations and Precedence
 
-The most basic syntax extension commands allow introducing new (or overloading existing) prefix, infix, and postfix operators.
+The most basic syntax extension commands allow introducing new (or
+overloading existing) prefix, infix, and postfix operators.
 
 ```lean
 infixl:65   " + " => HAdd.hAdd  -- left-associative
@@ -21,10 +32,15 @@ prefix:100  "-"   => Neg.neg
 postfix:max "⁻¹"  => Inv.inv
 ```
 
-After the initial command name describing the operator kind (its "fixity"), we give the *parsing precedence* of the operator preceded by a colon `:`, then a new or existing token surrounded by double quotes (the whitespace is used for pretty printing), then the function this operator should be translated to after the arrow `=>`.
+After the initial command name describing the operator kind (its
+"fixity"), we give the *parsing precedence* of the operator preceded
+by a colon `:`, then a new or existing token surrounded by double
+quotes (the whitespace is used for pretty printing), then the function
+this operator should be translated to after the arrow `=>`.
 
-The precedence is a natural number describing how "tightly" an operator binds to its arguments, encoding the order of operations.
-We can make this more precise by looking at the commands above unfold to:
+The precedence is a natural number describing how "tightly" an
+operator binds to its arguments, encoding the order of operations. We
+can make this more precise by looking at the commands above unfold to:
 
 ```lean
 notation:65 lhs:65 " + " rhs:66 => HAdd.hAdd lhs rhs
@@ -35,37 +51,58 @@ notation:100 "-" arg:100 => Neg.neg arg
 notation:1024 arg:1024 "⁻¹" => Inv.inv arg  -- `max` is a shorthand for precedence 1024
 ```
 
-It turns out that all commands from the first code block are in fact command *macros* translating to the more general `notation` command.
-We will learn about writing such macros below.
-Instead of a single token, the `notation` command accepts a mixed sequence of tokens and named term placeholders with precedences, which can be referenced on the right-hand side of `=>` and will be replaced by the respective term parsed at that position.
-A placeholder with precedence `p` accepts only notations with precedence at least `p` in that place.
-Thus the string `a + b + c` cannot be parsed as the equivalent of `a + (b + c)` because the right-hand side operand of an `infixl` notation has precedence one greater than the notation itself.
-In contrast, `infixr` reuses the notation's precedence for the right-hand side operand, so `a ^ b ^ c` *can* be parsed as `a ^ (b ^ c)`.
-Note that if we used `notation` directly to introduce an infix notation like
+It turns out that all commands from the first code block are in fact
+command *macros* translating to the more general `notation` command.
+We will learn about writing such macros below. Instead of a single
+token, the `notation` command accepts a mixed sequence of tokens and
+named term placeholders with precedences, which can be referenced on
+the right-hand side of `=>` and will be replaced by the respective
+term parsed at that position. A placeholder with precedence `p`
+accepts only notations with precedence at least `p` in that place.
+Thus the string `a + b + c` cannot be parsed as the equivalent of `a +
+(b + c)` because the right-hand side operand of an `infixl` notation
+has precedence one greater than the notation itself. In contrast,
+`infixr` reuses the notation's precedence for the right-hand side
+operand, so `a ^ b ^ c` *can* be parsed as `a ^ (b ^ c)`. Note that if
+we used `notation` directly to introduce an infix notation like
 ```lean
 # set_option quotPrecheck false
 notation:65 lhs:65 " ~ " rhs:65 => wobble lhs rhs
 ```
-where the precedences do not sufficiently determine associativity, Lean's parser will default to right associativity.
-More precisely, Lean's parser follows a local *longest parse* rule in the presence of ambiguous grammars: when parsing the right-hand side of `a ~` in `a ~ b ~ c`, it will continue parsing as long as possible (as the current precedence allows), not stopping after `b` but parsing `~ c` as well.
+where the precedences do not sufficiently determine associativity,
+Lean's parser will default to right associativity. More precisely,
+Lean's parser follows a local *longest parse* rule in the presence of
+ambiguous grammars: when parsing the right-hand side of `a ~` in `a ~
+b ~ c`, it will continue parsing as long as possible (as the current
+precedence allows), not stopping after `b` but parsing `~ c` as well.
 Thus the term is equivalent to `a ~ (b ~ c)`.
 
-As mentioned above, the `notation` command allows us to define arbitrary *mixfix* syntax freely mixing tokens and placeholders.
+As mentioned above, the `notation` command allows us to define
+arbitrary *mixfix* syntax freely mixing tokens and placeholders.
 ```lean
 # set_option quotPrecheck false
 notation:max "(" e ")" => e
 notation:10 Γ " ⊢ " e " : " τ => Typing Γ e τ
 ```
-Placeholders without precedence default to `0`, i.e. they accept notations of any precedence in their place.
-If two notations overlap, we again apply the longest parse rule:
+Placeholders without precedence default to `0`, i.e. they accept
+notations of any precedence in their place. If two notations overlap,
+we again apply the longest parse rule:
 ```lean
 notation:65 a " + " b:66 " + " c:66 => a + b - c
 #eval 1 + 2 + 3  -- 0
 ```
-The new notation is preferred to the binary notation since the latter, before chaining, would stop parsing after `1 + 2`.
-If there are multiple notations accepting the same longest parse, the choice will be delayed until elaboration, which will fail unless exactly one overload is type correct.
+The new notation is preferred to the binary notation since the latter,
+before chaining, would stop parsing after `1 + 2`. If there are
+multiple notations accepting the same longest parse, the choice will
+be delayed until elaboration, which will fail unless exactly one
+overload is type correct.
 
 ## Syntax and Macros
 ## Elaborators
 
-TODO. See [Lean Together 2021: Metaprogramming in Lean 4](https://youtu.be/hxQ1vvhYN_U) for an overview as well [the continuation](https://youtu.be/hxQ1vvhYN_U) about tactic programming. For more information on antiquotations, see also §4.1 of [Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages](https://arxiv.org/pdf/2001.10490.pdf#page=11).
+TODO. See [Lean Together 2021: Metaprogramming in Lean
+4](https://youtu.be/hxQ1vvhYN_U) for an overview as well [the
+continuation](https://youtu.be/hxQ1vvhYN_U) about tactic programming.
+For more information on antiquotations, see also §4.1 of [Beyond
+Notations: Hygienic Macro Expansion for Theorem Proving
+Languages](https://arxiv.org/pdf/2001.10490.pdf#page=11).
diff --git a/doc/types.md b/doc/types.md
new file mode 100644
index 0000000000..e685fba7d5
--- /dev/null
+++ b/doc/types.md
@@ -0,0 +1,56 @@
+# Types
+
+Every programming language needs a type system and
+Lean has a rich extensible inductive type system.
+
+## Basic Types
+
+Lean has built in support for the following basic types:
+
+- [Bool](bool.md) : a `true` or `false` value.
+- [Int](integers.md) : multiple precision integers (with no overflows!).
+
+- [Nat](integers.md) : natural numbers, or non-negative integers (also with no overflows!).
+- [Float](float.md): floating point numbers.
+- [Char](char.md): a Unicode character.
+- [String](string.md): a UTF-8 encoded string of characters.
+- [Array](array.md): a dynamic (aka growable) array of typed objects.
+- [List](list.md): a linked list of typed objects.
+- TODO: what else?
+
+And Lean allows you to create your own custom types using:
+- [Enumerated Types](enum.md): a special case of inductive types.
+- [Type Classes](typeclasses.md): a way of creating custom polymorphism.
+- [Types as objects](typeobjs.md): a way of manipulating types themselves.
+- [Structures](struct.md): a collection of named and typed fields. A
+  structure is actually special case of inductive datatype.
+- [Inductive Types](inductive.md): TODO: add one liner...
+
+## Universes
+
+Every type in Lean is, by definition, an expression of type `Sort u`
+for some universe level `u`. A universe level is one of the
+following:
+
+* a natural number, `n`
+* a universe variable, `u` (declared with the command `universe` or `universes`)
+* an expression `u + n`, where `u` is a universe level and `n` is a natural number
+* an expression `max u v`, where `u` and `v` are universes
+* an expression `imax u v`, where `u` and `v` are universe levels
+
+The last one denotes the universe level `0` if `v` is `0`, and `max u v` otherwise.
+
+```lean
+universe u v
+
+#check Sort u                       -- Type u
+#check Sort 5                       -- Type 4 : Type 5
+#check Sort (u + 1)                 -- Type u : Type (u + 1)
+#check Sort (u + 3)                 -- Type (u + 2) : Type (u + 3)
+#check Sort (max u v)               -- Sort (max u v) : Type (max u v)
+#check Sort (max (u + 3) v)         -- Sort (max (u + 3) v) : Type (max (u + 3) v)
+#check Sort (imax (u + 3) v)        -- Sort (imax (u + 3) v) : Type (imax (u + 3) v)
+#check Prop                         -- Type
+#check Type                         -- Type 1
+#check Type 1                       -- Type 1 : Type 2
+```
diff --git a/doc/whatIsLean.md b/doc/whatIsLean.md
index 326628c694..e1aff83156 100644
--- a/doc/whatIsLean.md
+++ b/doc/whatIsLean.md
@@ -32,10 +32,10 @@ Lean has numerous features, including:
 - First-class functions
 - Powerful data types
 - Pattern matching
-- Type classes
-- Extensible syntax
+- [Type classes](typeclass.md)
+- [Extensible syntax](syntax.md)
 - Hygienic macros
-- Dependent types
-- Metaprogramming framework
+- [Dependent types](deptypes.md)
+- [Metaprogramming framework](metaprogramming.md)
 - Multithreading
 - Verification: you can prove properties of your functions using Lean itself