format code: trim whitespace, add annotation

lean/main/05_syntax.lean

@@ -563,15 +563,15 @@ the bound variables, we refer the reader to the macro chapter.
 
 1. Create an "urgent minus 💀" notation such that `5 * 8 💀 4` returns `20`, and `8 💀 6 💀 1` returns `3`.
 
-    **a)** Using `notation` command.  
-    **b)** Using `infix` command.  
-    **c)** Using `syntax` command.  
+    **a)** Using `notation` command.
+    **b)** Using `infix` command.
+    **c)** Using `syntax` command.
 
     Hint: multiplication in Lean 4 is defined as `infixl:70 " * " => HMul.hMul`.
 
 2. Consider the following syntax categories: `term`, `command`, `tactic`; and 3 syntax rules given below. Make use of each of these newly defined syntaxes.
 
-    ```
+    ```lean
       syntax "good morning" : term
       syntax "hello" : command
       syntax "yellow" : tactic

lean/main/06_macros.lean

@@ -35,7 +35,7 @@ to indicate that "it doesn't feel responsible for this syntax". In this case
 it's merely used to fill a wildcard pattern that should never be reached anyways.
 
 However we can in fact register multiple macros for the same syntax this way
-if we desire, they will be tried one after another (the later registered ones have 
+if we desire, they will be tried one after another (the later registered ones have
 higher priority)  -- is "higher" correct?
 until one throws either a real error using `Macro.throwError` or succeeds, that
 is it does not `Macro.throwUnsupported`. Let's see this in action:
@@ -169,7 +169,7 @@ for example macro creating macros, we can escape the anti quotation using: `` `(
 If we want to specify the syntax kind we wish `x` to be interpreted as
 we can make this explicit using: `` `($x:term) `` where `term` can be
 replaced with any other valid syntax category (e.g. `command`) or parser
-(e.g. `ident`). 
+(e.g. `ident`).
 
 So far this is only a more formal explanation of the intuitive things
 we've already seen in the syntax chapter and up to now in this chapter,
@@ -198,11 +198,11 @@ For example:
 -/
 
 -- syntactically cut away the first element of a tuple if possible
-syntax "cut_tuple " "(" term ", " term,+ ")" : term 
+syntax "cut_tuple " "(" term ", " term,+ ")" : term
 
 macro_rules
   -- cutting away one element of a pair isn't possible, it would not result in a tuple
-  | `(cut_tuple ($x, $y)) => `(($x, $y)) 
+  | `(cut_tuple ($x, $y)) => `(($x, $y))
   | `(cut_tuple ($x, $y, $xs,*)) => `(($y, $xs,*))
 
 #check cut_tuple (1, 2) -- (1, 2) : Nat × Nat
@@ -225,7 +225,7 @@ we know so far we'd have to write two `macro_rules` now, one for the case
 with, one for the case without the optional argument. However the rest
 of the syntactic translation works exactly the same with and without
 the optional argument so what we can do using a splice here is to essentially
-define both cases at once: 
+define both cases at once:
 -/
 
 macro_rules

lean/main/07_elaboration.lean

@@ -173,7 +173,7 @@ elab "#findCElab " c:command : command => do
 /-!
 TODO: Maybe we should also add a mini project that demonstrates a
 non # style command aka a declaration, although nothing comes to mind right now.
-TODO:  Define a `conjecture` declaration, similar to `lemma/theorem`, except that 
+TODO:  Define a `conjecture` declaration, similar to `lemma/theorem`, except that
 it is automatically sorried.  The `sorry` could be a custom one, to reflect that
 the "conjecture" might be expected to be true.
 -/
@@ -316,7 +316,7 @@ def myanonImpl : TermElab := fun stx typ? => do
   -- Term elaborators can only postpone execution once, so the elaborator
   -- doesn't end up in an infinite loop. Hence, we only try to postpone it,
   -- otherwise we may cause an error.
-  tryPostponeIfNoneOrMVar typ? 
+  tryPostponeIfNoneOrMVar typ?
   -- If we haven't found the type after postponing just error
   let some typ := typ? | throwError "expected type must be known"
   if typ.isMVar then
@@ -338,7 +338,7 @@ syntax sugar of the `elab` syntax instead:
 -/
 
 -- This `t` syntax will effectively perform the first two lines of `myanonImpl`
-elab "⟨⟨" args:term,* "⟩⟩" : term <= t => do 
+elab "⟨⟨" args:term,* "⟩⟩" : term <= t => do
   sorry
 
 
@@ -377,8 +377,8 @@ elab "⟨⟨" args:term,* "⟩⟩" : term <= t => do
 
     Please add these semantics:
 
-    **a)** using `syntax` + `@[command_elab alias] def elabOurAlias : CommandElab`.  
-    **b)** using `syntax` + `elab_rules`.  
+    **a)** using `syntax` + `@[command_elab alias] def elabOurAlias : CommandElab`.
+    **b)** using `syntax` + `elab_rules`.
     **c)** using `elab`.
 
 3. Here is some syntax taken from a real mathlib tactic `nth_rewrite`.
@@ -392,8 +392,8 @@ elab "⟨⟨" args:term,* "⟩⟩" : term <= t => do
 
     Please add these semantics:
 
-    **a)** using `syntax` + `@[tactic nthRewrite] def elabNthRewrite : Lean.Elab.Tactic.Tactic`.  
-    **b)** using `syntax` + `elab_rules`.  
+    **a)** using `syntax` + `@[tactic nthRewrite] def elabNthRewrite : Lean.Elab.Tactic.Tactic`.
+    **b)** using `syntax` + `elab_rules`.
     **c)** using `elab`.
 
 -/

lean/main/09_tactics.lean

@@ -593,9 +593,9 @@ tactic infrastructure and the parsing front-end.
 ## Exercises
 
 1. Consider the theorem `p ∧ q ↔ q ∧ p`. We could either write its proof as a proof term, or construct it using the tactics.
-    When we are writing the proof of this theorem *as a proof term*, we're gradually filling up `_`s with certain expressions, step by step. Each such step corresponds to a tactic.  
+    When we are writing the proof of this theorem *as a proof term*, we're gradually filling up `_`s with certain expressions, step by step. Each such step corresponds to a tactic.
 
-    There are many combinations of steps in which we could write this proof term - but consider the sequence of steps we wrote below. Please write each step as a tactic.  
+    There are many combinations of steps in which we could write this proof term - but consider the sequence of steps we wrote below. Please write each step as a tactic.
     The tactic `step_1` is filled in, please do the same for the remaining tactics (for the sake of the exercise, try to use lower-level apis, such as `mkFreshExprMVar`, `mvarId.assign` and `modify fun _ => { goals := ~)`.
 
     ```lean
@@ -653,7 +653,7 @@ tactic infrastructure and the parsing front-end.
 
       -- 1. Create new `_`s with appropriate types.
       let mvarId1 ← mkFreshExprMVar (Expr.forallE `xxx a b .default) (userName := "red")
-      let mvarId2 ← mkFreshExprMVar (Expr.forallE `yyy b a .default) (userName := "blue") 
+      let mvarId2 ← mkFreshExprMVar (Expr.forallE `yyy b a .default) (userName := "blue")
 
       -- 2. Assign the main goal to the expression `Iff.intro _ _`.
       mvarId.assign (mkAppN (Expr.const `Iff.intro []) #[a, b, mvarId1, mvarId2])
@@ -670,13 +670,13 @@ tactic infrastructure and the parsing front-end.
       step_4
     ```
 
-2. In the first exercise, we used lower-level `modify` api to update our goals.  
-    `liftMetaTactic`, `setGoals`, `appendGoals`, `replaceMainGoal`, `closeMainGoal`, etc. are all syntax sugars on top of `modify fun s : State => { s with goals := myMvarIds }`.  
-    Please rewrite the `forker` tactic with:  
+2. In the first exercise, we used lower-level `modify` api to update our goals.
+    `liftMetaTactic`, `setGoals`, `appendGoals`, `replaceMainGoal`, `closeMainGoal`, etc. are all syntax sugars on top of `modify fun s : State => { s with goals := myMvarIds }`.
+    Please rewrite the `forker` tactic with:
 
-    **a)** `liftMetaTactic`  
-    **b)** `setGoals`  
-    **c)** `replaceMainGoal`  
+    **a)** `liftMetaTactic`
+    **b)** `setGoals`
+    **c)** `replaceMainGoal`
 
     ```lean
     elab "forker" : tactic => do
@@ -709,9 +709,9 @@ tactic infrastructure and the parsing front-end.
 
     For each of the points below, create a tactic `introductor` (one per each point), that turns the goal `(ab: a = b) → (bc: b = c) → (a = c)`:
 
-    **a)** into the goal `(a = c)` with hypotheses `(ab✝: a = b)` and `(bc✝: b = c)`.  
-    **b)** into the goal `(bc: b = c) → (a = c)` with hypothesis `(ab: a = b)`.  
-    **c)** into the goal `(bc: b = c) → (a = c)` with hypothesis `(hello: a = b)`.  
+    **a)** into the goal `(a = c)` with hypotheses `(ab✝: a = b)` and `(bc✝: b = c)`.
+    **b)** into the goal `(bc: b = c) → (a = c)` with hypothesis `(ab: a = b)`.
+    **c)** into the goal `(bc: b = c) → (a = c)` with hypothesis `(hello: a = b)`.
 
     ```lean
     example (a b c : Nat) : (ab: a = b) → (bc: b = c) → (a = c) := by