doc: clean up examples markup

doc/examples/bintree.lean

@@ -1,7 +1,5 @@
 /-|
-==========================================
-Binary Search Trees
-==========================================
+# Binary Search Trees
 
 If the type of keys can be totally ordered -- that is, it supports a well-behaved `≤` comparison --
 then maps can be implemented with binary search trees (BSTs). Insert and lookup operations on BSTs take time
@@ -101,17 +99,17 @@ We now prove that `t.toList` and `t.toListTR` return the same list.
 The proof is on induction, and as we used the auxiliary function `go`
 to define `Tree.toListTR`, we use the auxiliary theorem `go` to prove the theorem.
 
-The proof of the auxiliary theorem is by induction on `t`\ .
-The `generalizing acc` modifier instructs Lean to revert `acc`\ , apply the
-induction theorem for `Tree`\ s, and then reintroduce `acc` in each case.
-By using `generalizing`\ , we obtain the more general induction hypotheses
+The proof of the auxiliary theorem is by induction on `t`.
+The `generalizing acc` modifier instructs Lean to revert `acc`, apply the
+induction theorem for `Tree`s, and then reintroduce `acc` in each case.
+By using `generalizing`, we obtain the more general induction hypotheses
 
 - `left_ih : ∀ acc, toListTR.go left acc = toList left ++ acc`
 
 - `right_ih : ∀ acc, toListTR.go right acc = toList right ++ acc`
 
 Recall that the combinator `tac <;> tac'` runs `tac` on the main goal and `tac'` on each produced goal,
-concatenating all goals produced by `tac'`\ . In this theorem, we use it to apply
+concatenating all goals produced by `tac'`. In this theorem, we use it to apply
 `simp` and close each subgoal produced by the `induction` tactic.
 
 The `simp` parameters `toListTR.go` and `toList` instruct the simplifier to try to reduce
@@ -237,7 +235,7 @@ theorem Tree.bst_insert_of_bst
         exact .node h₁ h₂ b₁ b₂
 
 /-|
-Now, we define the type `BinTree` using a `Subtype` that states that only trees satisfying the BST invariant are `BinTree`\ s.
+Now, we define the type `BinTree` using a `Subtype` that states that only trees satisfying the BST invariant are `BinTree`s.
 -/
 def BinTree (β : Type u) := { t : Tree β // BST t }
 

doc/examples/deBruijn.lean

@@ -1,7 +1,5 @@
 /-|
-==========================================
-Dependent de Bruijn Indices
-==========================================
+# Dependent de Bruijn Indices
 
 In this example, we represent program syntax terms in a type family parameterized by a list of types,
 representing the typing context, or information on which free variables are in scope and what

doc/examples/interp.lean

@@ -1,7 +1,5 @@
 /-|
-==========================================
-The Well-Typed Interpreter
-==========================================
+# The Well-Typed Interpreter
 
 In this example, we build an interpreter for a simple functional programming language,
 with variables, function application, binary operators and an `if...then...else` construct.
@@ -22,7 +20,7 @@ inductive Vector (α : Type u) : Nat → Type u
   | cons : α → Vector α n → Vector α (n+1)
 
 /-|
-We can overload the `List.cons` notation `::` and use it to create `Vector`\ s.
+We can overload the `List.cons` notation `::` and use it to create `Vector`s.
 -/
 infix:67 " :: " => Vector.cons
 

doc/examples/palindromes.lean

@@ -1,14 +1,12 @@
 /-|
-==========================================
-Palindromes
-==========================================
+# Palindromes
 
 Palindromes are lists that read the same from left to right and from right to left.
 For example, `[a, b, b, a]` and `[a, h, a]` are palindromes.
 
 We use an inductive predicate to specify whether a list is a palindrome or not.
 Recall that inductive predicates, or inductively defined propositions, are a convenient
-way to specify functions of type `... → Prop`\ .
+way to specify functions of type `... → Prop`.
 
 This example is a based on an example from the book "The Hitchhiker's Guide to Logical Verification".
 -/
@@ -25,7 +23,7 @@ The definition distinguishes three cases: (1) `[]` is a palindrome; (2) for any
 -/
 
 /-|
-We now prove that the reverse of a palindrome is a palindrome using induction on the inductive predicate `h : Palindrome as`\ .
+We now prove that the reverse of a palindrome is a palindrome using induction on the inductive predicate `h : Palindrome as`.
 -/
 theorem palindrome_reverse (h : Palindrome as) : Palindrome as.reverse := by
   induction h with
@@ -66,8 +64,8 @@ We use the attribute `@[simp]` to instruct the `simp` tactic to use this theorem
     exact dropLast_append_last (as := a₂ :: as) (by simp)
 
 /-|
-We now define the following auxiliary induction principle for lists using well-founded recursion on `as.length`\ .
-We can read it as follows, to prove `motive as`, it suffices to show that: (1) `motive []`\ ; (2) `motive [a]` for any `a`;
+We now define the following auxiliary induction principle for lists using well-founded recursion on `as.length`.
+We can read it as follows, to prove `motive as`, it suffices to show that: (1) `motive []`; (2) `motive [a]` for any `a`;
 (3) if `motive as` holds, then `motive ([a] ++ as ++ [b])` also holds for any `a`, `b`, and `as`.
 Note that the structure of this induction principle is very similar to the `Palindrome` inductive predicate.
 -/

doc/examples/phoas.lean

@@ -1,7 +1,5 @@
 /-|
-==========================================
-Parametric Higher-Order Abstract Syntax
-==========================================
+# Parametric Higher-Order Abstract Syntax
 
 In contrast to first-order encodings, higher-order encodings avoid explicit modeling of variable identity.
 Instead, the binding constructs of an object language (the language being

doc/examples/tc.lean

@@ -1,7 +1,5 @@
 /-|
-==========================================
-A Certified Type Checker
-==========================================
+# A Certified Type Checker
 
 In this example, we build a certified type checker for a simple expression
 language.