doc: add slide headers to examples

doc/examples/NFM2022/nfm1.lean

@@ -1,3 +1,5 @@
+/- "Hello world" -/
+
 #eval "hello" ++ " " ++ "world"
 -- "hello world"
 

doc/examples/NFM2022/nfm10.lean

@@ -1,3 +1,5 @@
+/- Dependent pattern matching -/
+
 inductive Vector (α : Type u) : Nat → Type u
   | nil : Vector α 0
   | cons : α → Vector α n → Vector α (n+1)

doc/examples/NFM2022/nfm11.lean

@@ -1,3 +1,5 @@
+/- Structures -/
+
 structure Point where
   x : Int := 0
   y : Int := 0

doc/examples/NFM2022/nfm12.lean

@@ -1,3 +1,4 @@
+/- Type classes -/
 namespace Example
 
 class ToString (α : Type u) where

doc/examples/NFM2022/nfm13.lean

@@ -1,3 +1,4 @@
+/- Type classes are heavily used in Lean -/
 namespace Example
 
 class Mul (α : Type u) where
@@ -26,3 +27,18 @@ class LawfulFunctor (f : Type u → Type v) [Functor f] : Prop where
   comp_map (g : α → β) (h : β → γ) (x : f α) :(h ∘ g) <$> x = h <$> g <$> x
 
 end Example
+
+/-
+`Deriving instances automatically`
+
+We have seen `deriving Repr` in a few examples.
+It is an instance generator.
+Lean comes equipped with generators for the following classes.
+`Repr`, `Inhabited`, `BEq`, `DecidableEq`,
+`Hashable`, `Ord`, `FromToJson`, `SizeOf`
+-/
+
+inductive Tree (α : Type u) where
+  | leaf (val : α)
+  | node (left right : Tree α)
+  deriving DecidableEq, Ord, Inhabited, Repr

doc/examples/NFM2022/nfm14.lean

@@ -1,3 +1,5 @@
+/- Tactics -/
+
 example : p → q → p ∧ q ∧ p := by
   intro hp hq
   apply And.intro
@@ -9,6 +11,8 @@ example : p → q → p ∧ q ∧ p := by
 example : p → q → p ∧ q ∧ p := by
   intro hp hq; apply And.intro hp; exact And.intro hq hp
 
+/- Structuring proofs -/
+
 example : p → q → p ∧ q ∧ p := by
   intro hp hq
   apply And.intro

doc/examples/NFM2022/nfm15.lean

@@ -1,3 +1,4 @@
+/- intro tactic variants -/
 
 example (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by
   intro h

doc/examples/NFM2022/nfm16.lean

@@ -1,3 +1,5 @@
+/- Inaccessible names -/
+
 example : ∀ x y : Nat, x = y → y = x := by
   intros
   apply Eq.symm

doc/examples/NFM2022/nfm17.lean

@@ -1,3 +1,5 @@
+/- More tactics -/
+
 example (p q : Nat → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by
   intro h
   cases h with

doc/examples/NFM2022/nfm18.lean

@@ -1,3 +1,5 @@
+/- Structuring proofs (cont.) -/
+
 example : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by
   intro h
   have hp : p := h.left

doc/examples/NFM2022/nfm19.lean

@@ -1,3 +1,5 @@
+/- Tactic combinators -/
+
 example : p → q → r → p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by
   intros
   repeat (any_goals constructor)

doc/examples/NFM2022/nfm2.lean

@@ -1,3 +1,5 @@
+/- First-class functions -/
+
 def twice (f : Nat → Nat) (a : Nat) :=
   f (f a)
 

doc/examples/NFM2022/nfm20.lean

@@ -1,3 +1,5 @@
+/- Rewriting -/
+
 example (f : Nat → Nat) (k : Nat) (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := by
   rw [h₂] -- replace k with 0
   rw [h₁] -- replace f 0 with 0

doc/examples/NFM2022/nfm21.lean

@@ -1,3 +1,5 @@
+/- Simplifier -/
+
 example (p : Nat → Prop) : (x + 0) * (0 + y * 1 + z * 0) = x * y := by
   simp
 

doc/examples/NFM2022/nfm22.lean

@@ -1,8 +1,10 @@
+/- Simplifier -/
+
 def mk_symm (xs : List α) :=
- xs ++ xs.reverse
+  xs ++ xs.reverse
 
 @[simp] theorem reverse_mk_symm : (mk_symm xs).reverse = mk_symm xs := by
- simp [mk_symm]
+  simp [mk_symm]
 
 theorem tst : (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse := by
   simp

doc/examples/NFM2022/nfm23.lean

@@ -1,3 +1,5 @@
+/- split tactic -/
+
 def f (x y z : Nat) : Nat :=
   match x, y, z with
   | 5, _, _ => y

doc/examples/NFM2022/nfm24.lean

@@ -1,4 +1,4 @@
-
+/- induction tactic -/
 
 example (as : List α) (a : α) : (as.concat a).length = as.length + 1 := by
   induction as with

doc/examples/NFM2022/nfm3.lean

@@ -1,3 +1,5 @@
+/- Enumerated types -/
+
 inductive Weekday where
   | sunday | monday | tuesday | wednesday
   | thursday | friday | saturday
@@ -37,6 +39,8 @@ def Weekday.previous : Weekday → Weekday
   | friday    => thursday
   | saturday  => friday
 
+/- Proving theorems using tactics -/
+
 theorem Weekday.next_previous (d : Weekday) : d.next.previous = d :=
   match d with
   | sunday    => rfl

doc/examples/NFM2022/nfm4.lean

@@ -1,3 +1,4 @@
+/- What is the type of Nat? -/
 
 #check 0
 -- Nat

doc/examples/NFM2022/nfm5.lean

@@ -1,3 +1,5 @@
+/- Implicit arguments and universe polymorphism -/
+
 def f (α β : Sort u) (a : α) (b : β) : α := a
 
 #eval f Nat String 1 "hello"

doc/examples/NFM2022/nfm6.lean

@@ -1,3 +1,4 @@
+/- Inductive Types -/
 
 inductive Tree (β : Type v) where
   | leaf

doc/examples/NFM2022/nfm7.lean

@@ -1,3 +1,5 @@
+/- Recursive functions -/
+
 #print Nat -- Nat is an inductive datatype
 
 def fib (n : Nat) : Nat :=

doc/examples/NFM2022/nfm8.lean

@@ -1,3 +1,5 @@
+/- Well-founded recursion -/
+
 def ack : Nat → Nat → Nat
   | 0,   y   => y+1
   | x+1, 0   => ack x 1

doc/examples/NFM2022/nfm9.lean

@@ -1,3 +1,5 @@
+/- Mutual recursion -/
+
 inductive Term where
  | const : String → Term
  | app   : String → List Term → Term
@@ -7,6 +9,7 @@ mutual
  def numConsts : Term → Nat
    | const _ => 1
    | app _ cs => numConstsLst cs
+
  def numConstsLst : List Term → Nat
    | [] => 0
    | c :: cs => numConsts c + numConstsLst cs
@@ -22,6 +25,8 @@ mutual
    | c :: cs => replaceConst a b c :: replaceConstLst a b cs
 end
 
+/- Mutual recursion in theorems -/
+
 mutual
   theorem numConsts_replaceConst (a b : String) (e : Term)
             : numConsts (replaceConst a b e) = numConsts e := by