Small typos and formatting (#113)

axioms_and_computation.md

@@ -192,7 +192,7 @@ Function Extensionality
 
 Similar to propositional extensionality, function extensionality
 asserts that any two functions of type ``(x : α) → β x`` that agree on
-all their inputs are equal.
+all their inputs are equal:
 
 ```lean
 universe u v
@@ -285,7 +285,7 @@ theorem inter.comm (a b : Set α) : a ∩ b = b ∩ a :=
 ```
 
 The following is an example of how function extensionality blocks
-computation inside the Lean kernel.
+computation inside the Lean kernel:
 
 ```lean
 def f (x : Nat) := x
@@ -315,7 +315,7 @@ nontrivial examples, eliminating cast changes the type of the term,
 which might make an ambient expression type incorrect. The virtual
 machine, however, has no trouble evaluating the expression to
 ``0``. Here is a similarly contrived example that shows how
-``propext`` can get in the way.
+``propext`` can get in the way:
 
 ```lean
 theorem tteq : (True ∧ True) = True :=
@@ -334,14 +334,14 @@ def val : Nat :=
 Current research programs, including work on *observational type
 theory* and *cubical type theory*, aim to extend type theory in ways
 that permit reductions for casts involving function extensionality,
-quotients, and more. But the solutions are not so clear cut, and the
+quotients, and more. But the solutions are not so clear-cut, and the
 rules of Lean's underlying calculus do not sanction such reductions.
 
 In a sense, however, a cast does not change the meaning of an
 expression. Rather, it is a mechanism to reason about the expression's
 type. Given an appropriate semantics, it then makes sense to reduce
 terms in ways that preserve their meaning, ignoring the intermediate
-bookkeeping needed to make the reductions type correct. In that case,
+bookkeeping needed to make the reductions type-correct. In that case,
 adding new axioms in ``Prop`` does not matter; by proof irrelevance,
 an expression in ``Prop`` carries no information, and can be safely
 ignored by the reduction procedures.

conv.md

@@ -2,7 +2,7 @@ The Conversion Tactic Mode
 =========================
 
 Inside a tactic block, one can use the keyword `conv` to enter
-conversion mode. This mode allows to travel inside assumptions and
+*conversion mode*. This mode allows to travel inside assumptions and
 goals, even inside function abstractions and dependent arrows, to apply rewriting or
 simplifying steps.
 
@@ -35,7 +35,8 @@ example (a b c : Nat) : a * (b * c) = a * (c * b) := by
 
 The above snippet shows three navigation commands:
 
-- `lhs` navigates to the left hand side of a relation (here equality), there is also a `rhs` navigating to the right hand side.
+- `lhs` navigates to the left-hand side of a relation (equality, in this case).
+   There is also a `rhs` to navigate to the right-hand side.
 - `congr` creates as many targets as there are (nondependent and explicit) arguments to the current head function
   (here the head function is multiplication).
 - `rfl` closes target using reflexivity.
@@ -112,7 +113,7 @@ example (a b c : Nat) : a * (b * c) = a * (c * b) := by
 Structuring conversion tactics
 -------
 
-Curly brackets and `.` can also be used in `conv` mode to structure tactics.
+Curly brackets and `.` can also be used in `conv` mode to structure tactics:
 
 ```lean
 example (a b c : Nat) : (0 + a) * (b * c) = a * (c * b) := by
@@ -192,7 +193,7 @@ example (g : Nat → Nat → Nat)
     . tactic => exact h₂
 ```
 
-- `apply <term>` is syntax sugar for `tactic => apply <term>`
+- `apply <term>` is syntax sugar for `tactic => apply <term>`.
 
 ```lean
 example (g : Nat → Nat → Nat)

dependent_type_theory.md

@@ -224,8 +224,8 @@ hierarchy of types:
 Think of ``Type 0`` as a universe of "small" or "ordinary" types.
 ``Type 1`` is then a larger universe of types, which contains ``Type
 0`` as an element, and ``Type 2`` is an even larger universe of types,
-which contains ``Type 1`` as an element. The list is indefinite, so
-that there is a ``Type n`` for every natural number ``n``. ``Type`` is
+which contains ``Type 1`` as an element. The list is infinite:
+there is a ``Type n`` for every natural number ``n``. ``Type`` is
 an abbreviation for ``Type 0``:
 
 ```lean
@@ -275,7 +275,7 @@ def F (α : Type u) : Type u := Prod α α
 #check F    -- Type u → Type u
 ```
 
-You can avoid the universe command by providing the universe parameters when defining F.
+You can avoid the `universe` command by providing the universe parameters when defining `F`:
 
 ```lean
 def F.{u} (α : Type u) : Type u := Prod α α
@@ -359,7 +359,7 @@ The last expression, for example, denotes the function that takes
 three types, ``α``, ``β``, and ``γ``, and two functions, ``g : β → γ``
 and ``f : α → β``, and returns the composition of ``g`` and ``f``.
 (Making sense of the type of this function requires an understanding
-of dependent products, which will be explained below.)
+of *dependent products*, which will be explained below.)
 
 The general form of a lambda expression is ``fun x : α => t``, where
 the variable ``x`` is a "bound variable": it is really a placeholder,
@@ -935,7 +935,7 @@ Suppose we have an implementation of lists as:
 #check Lst.append   -- Lst.append.{u} (α : Type u) (as bs : Lst α) : Lst α
 ```
 
-Then, you can construct lists of `Nat` as follows.
+Then, you can construct lists of `Nat` as follows:
 
 ```lean
 # universe u

induction_and_recursion.md

@@ -688,7 +688,7 @@ if ``x`` has no predecessors, it is accessible. Given any type ``α``,
 we should be able to assign a value to each accessible element of
 ``α``, recursively, by assigning values to all its predecessors first.
 
-The statement that ``r`` is well founded, denoted ``WellFounded r``,
+The statement that ``r`` is well-founded, denoted ``WellFounded r``,
 is exactly the statement that every element of the type is
 accessible. By the above considerations, if ``r`` is a well-founded
 relation on a type ``α``, we should have a principle of well-founded
@@ -707,15 +707,15 @@ noncomputable def f {α : Sort u}
 
 There is a long cast of characters here, but the first block we have
 already seen: the type, ``α``, the relation, ``r``, and the
-assumption, ``h``, that ``r`` is well founded. The variable ``C``
+assumption, ``h``, that ``r`` is well-founded. The variable ``C``
 represents the motive of the recursive definition: for each element
 ``x : α``, we would like to construct an element of ``C x``. The
 function ``F`` provides the inductive recipe for doing that: it tells
 us how to construct an element ``C x``, given elements of ``C y`` for
 each predecessor ``y`` of ``x``.
 
 Note that ``WellFounded.fix`` works equally well as an induction
-principle. It says that if ``≺`` is well founded and you want to prove
+principle. It says that if ``≺`` is well-founded and you want to prove
 ``∀ x, C x``, it suffices to show that for an arbitrary ``x``, if we
 have ``∀ y ≺ x, C y``, then we have ``C x``.
 
@@ -810,7 +810,7 @@ def natToBin : Nat → List Nat
 ```
 
 As a final example, we observe that Ackermann's function can be
-defined directly, because it is justified by the well foundedness of
+defined directly, because it is justified by the well-foundedness of
 the lexicographic order on the natural numbers. The `termination_by` clause
 instructs Lean to use a lexicographic order. This clause is actually mapping
 the function arguments to elements of type `Nat × Nat`. Then, Lean uses typeclass
@@ -894,7 +894,8 @@ decreasing_by sorry
 #eval natToBin 1234567
 ```
 
-Recall that using `sorry` is equivalent to using a new axiom, and should be avoided. In the following example, we used the `sorry` to prove `False`. The command `#print axioms` shows that `unsound` depends on the unsound axiom `sorryAx` used to implement `sorry`.
+Recall that using `sorry` is equivalent to using a new axiom, and should be avoided. In the following example, we used the `sorry` to prove `False`.
+The command `#print axioms unsound` shows that `unsound` depends on the unsound axiom `sorryAx` used to implement `sorry`.
 
 ```lean
 def unsound (x : Nat) : False :=
@@ -1348,7 +1349,7 @@ Match Expressions
 -----------------
 
 Lean also provides a compiler for *match-with* expressions found in
-many functional languages.
+many functional languages:
 
 ```lean
 def isNotZero (m : Nat) : Bool :=
@@ -1393,7 +1394,7 @@ example : foo 7 true false = 9 := rfl
 ```
 
 Lean uses the ``match`` construct internally to implement pattern-matching in all parts of the system.
-Thus, all four of these definitions have the same net effect.
+Thus, all four of these definitions have the same net effect:
 
 ```lean
 def bar₁ : Nat × Nat → Nat
@@ -1436,7 +1437,7 @@ example (h₀ : ∃ x, p x) (h₁ : ∃ y, q y)
 Local Recursive Declarations
 ---------
 
-You can define local recursive declarations using the `let rec` keyword.
+You can define local recursive declarations using the `let rec` keyword:
 
 ```lean
 def replicate (n : Nat) (a : α) : List α :=
@@ -1455,7 +1456,7 @@ Note that, Lean "closes" the declaration by adding any local variable occurring
 `let rec` declaration as additional parameters. For example, the local variable `a` occurs
 at `let rec loop`.
 
-You can also use `let rec` in tactic mode and for creating proofs by induction.
+You can also use `let rec` in tactic mode and for creating proofs by induction:
 
 ```lean
 # def replicate (n : Nat) (a : α) : List α :=
@@ -1473,7 +1474,7 @@ theorem length_replicate (n : Nat) (a : α) : (replicate n a).length = n := by
 ```
 
 You can also introduce auxiliary recursive declarations using a `where` clause after your definition.
-Lean converts them into a `let rec`.
+Lean converts them into a `let rec`:
 
 ```lean
 def replicate (n : Nat) (a : α) : List α :=

interacting_with_lean.md

@@ -17,8 +17,8 @@ Importing Files
 ---------------
 
 The goal of Lean's front end is to interpret user input, construct
-formal expressions, and check that they are well formed and type
-correct. Lean also supports the use of various editors, which provide
+formal expressions, and check that they are well-formed and type-correct.
+Lean also supports the use of various editors, which provide
 continuous checking and feedback. More information can be found on the
 Lean [documentation pages](https://lean-lang.org/documentation/).
 
@@ -213,7 +213,7 @@ stored in the environment for later use. But some commands have other
 effects on the environment, either assigning attributes to objects in
 the environment, defining notation, or declaring instances of type
 classes, as described in [Chapter Type Classes](./type_classes.md). Most of
-these commands have global effects, which is to say, that they remain
+these commands have global effects, which is to say, they remain
 in effect not only in the current file, but also in any file that
 imports it. However, such commands often support the ``local`` modifier,
 which indicates that they only have effect until
@@ -542,7 +542,7 @@ 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.
+overload is type-correct.
 
 Coercions
 ---------

propositions_and_proofs.md

@@ -51,7 +51,7 @@ variable (p q : Prop)
 
 In addition to axioms, however, we would also need rules to build new
 proofs from old ones. For example, in many proof systems for
-propositional logic, we have the rule of modus ponens:
+propositional logic, we have the rule of *modus ponens*:
 
 > From a proof of ``Implies p q`` and a proof of ``p``, we obtain a proof of ``q``.
 
@@ -202,13 +202,13 @@ theorem is complete, typically we only need to know that the proof
 exists; it doesn't matter what the proof is. In light of that fact,
 Lean tags proofs as *irreducible*, which serves as a hint to the
 parser (more precisely, the *elaborator*) that there is generally no
-need to unfold it when processing a file. In fact, Lean is generally
+need to unfold them when processing a file. In fact, Lean is generally
 able to process and check proofs in parallel, since assessing the
 correctness of one proof does not require knowing the details of
 another.
 
 As with definitions, the ``#print`` command will show you the proof of
-a theorem.
+a theorem:
 
 ```lean
 # variable {p : Prop}
@@ -221,7 +221,7 @@ theorem t1 : p → q → p := fun hp : p => fun hq : q => hp
 Notice that the lambda abstractions ``hp : p`` and ``hq : q`` can be
 viewed as temporary assumptions in the proof of ``t1``.  Lean also
 allows us to specify the type of the final term ``hp``, explicitly,
-with a ``show`` statement.
+with a ``show`` statement:
 
 ```lean
 # variable {p : Prop}
@@ -248,7 +248,7 @@ theorem t1 (hp : p) (hq : q) : p := hp
 #print t1    -- p → q → p
 ```
 
-Now we can apply the theorem ``t1`` just as a function application.
+We can use the theorem ``t1`` just as a function application:
 
 ```lean
 # variable {p : Prop}
@@ -260,10 +260,10 @@ axiom hp : p
 theorem t2 : q → p := t1 hp
 ```
 
-Here, the ``axiom`` declaration postulates the existence of an
+The ``axiom`` declaration postulates the existence of an
 element of the given type and may compromise logical consistency. For
-example, we can use it to postulate the empty type `False` has an
-element.
+example, we can use it to postulate that the empty type `False` has an
+element:
 
 ```lean
 axiom unsound : False