diff --git a/Manual/Classes.lean b/Manual/Classes.lean
index e8c49e4..9f1360f 100644
--- a/Manual/Classes.lean
+++ b/Manual/Classes.lean
@@ -273,7 +273,7 @@ def Heap.bubbleUp [Ord α] (i : Nat) (xs : Heap α) : Heap α :=
   else
     let j := i / 2
     if Ord.compare xs.contents[i] xs.contents[j] == .lt then
-      Heap.bubbleUp j {xs with contents := xs.contents.swap ⟨i, by omega⟩ ⟨j, by omega⟩}
+      Heap.bubbleUp j {xs with contents := xs.contents.swap i j}
     else xs
 
 def Heap.insert [Ord α] (x : α) (xs : Heap α) : Heap α :=
@@ -294,13 +294,12 @@ def Heap'.bubbleUp [inst : Ord α] (i : Nat) (xs : @Heap' α inst) : @Heap' α i
   else
     let j := i / 2
     if inst.compare xs.contents[i] xs.contents[j] == .lt then
-      Heap'.bubbleUp j {xs with contents := xs.contents.swap ⟨i, by omega⟩ ⟨j, by omega⟩}
+      Heap'.bubbleUp j {xs with contents := xs.contents.swap i j}
     else xs
 
 def Heap'.insert [Ord α] (x : α) (xs : Heap' α) : Heap' α :=
   let i := xs.contents.size
   {xs with contents := xs.contents.push x}.bubbleUp i
-end A
 ```
 
 In the improved definitions, {name}`Heap'.bubbleUp` is needlessly explicit; the instance does not need to be explicitly named here because Lean would select the indicated instances nonetheless, but it does bring the correctness invariant front and center for readers.
diff --git a/Manual/Classes/InstanceDecls.lean b/Manual/Classes/InstanceDecls.lean
index 13d1d77..a2b1166 100644
--- a/Manual/Classes/InstanceDecls.lean
+++ b/Manual/Classes/InstanceDecls.lean
@@ -268,8 +268,10 @@ However, because it is an ordinary Lean function, it can recursively refer to it
 instance instDecidableEqStringList : DecidableEq StringList
   | .nil, .nil => .isTrue rfl
   | .cons h1 t1, .cons h2 t2 =>
+    let _ : Decidable (t1 = t2) :=
+      instDecidableEqStringList t1 t2
     if h : h1 = h2 then
-      if h' : instDecidableEqStringList t1 t2 then
+      if h' : t1 = t2 then
         .isTrue (by simp [*])
       else
         .isFalse (by intro hEq; cases hEq; trivial)
diff --git a/Manual/Language.lean b/Manual/Language.lean
index 89f4b51..bf6b71b 100644
--- a/Manual/Language.lean
+++ b/Manual/Language.lean
@@ -301,7 +301,7 @@ open Greetings
 
 The section's name must be used to close it.
 
-```lean (error := true) (name := english4)
+```lean (error := true) (name := english4) (keep := false)
 end
 ```
 ```leanOutput english4
diff --git a/Manual/Meta/Lean.lean b/Manual/Meta/Lean.lean
index 2ca647e..e186ad7 100644
--- a/Manual/Meta/Lean.lean
+++ b/Manual/Meta/Lean.lean
@@ -292,7 +292,7 @@ def leanInline : RoleExpander
     let expectedType ← config.type.mapM fun (s : StrLit) => do
       match Parser.runParserCategory (← getEnv) `term s.getString (← getFileName) with
       | .error e => throwErrorAt term e
-      | .ok stx => withEnableInfoTree false do
+      | .ok stx => withEnableInfoTree false <| runWithOpenDecls <| runWithVariables fun _ => do
         let t ← Elab.Term.elabType stx
         Term.synthesizeSyntheticMVarsNoPostponing
         let t ← instantiateMVars t
@@ -917,14 +917,18 @@ def name : RoleExpander
     let exampleName := name.getString.toName
     let identStx := mkIdentFrom arg (cfg.full.getD exampleName) (canonical := true)
 
-    let resolvedName ←
-      runWithOpenDecls <| runWithVariables fun _ =>
-        withInfoTreeContext (mkInfoTree := pure ∘ InfoTree.node (.ofCommandInfo {elaborator := `Manual.Meta.name, stx := identStx})) do
-          realizeGlobalConstNoOverloadWithInfo identStx
+    try
+      let resolvedName ←
+        runWithOpenDecls <| runWithVariables fun _ =>
+          withInfoTreeContext (mkInfoTree := pure ∘ InfoTree.node (.ofCommandInfo {elaborator := `Manual.Meta.name, stx := identStx})) do
+            realizeGlobalConstNoOverloadWithInfo identStx
 
-    let hl : Highlighted ← constTok resolvedName name.getString
+      let hl : Highlighted ← constTok resolvedName name.getString
 
-    pure #[← `(Inline.other {Inline.name with data := ToJson.toJson $(quote hl)} #[Inline.code $(quote name.getString)])]
+      pure #[← `(Inline.other {Inline.name with data := ToJson.toJson $(quote hl)} #[Inline.code $(quote name.getString)])]
+    catch e =>
+      logErrorAt identStx e.toMessageData
+      pure #[← `(Inline.code $(quote name.getString))]
   | _, more =>
     if h : more.size > 0 then
       throwErrorAt more[0] "Unexpected contents"
diff --git a/Manual/Meta/Lean/Scopes.lean b/Manual/Meta/Lean/Scopes.lean
index b73d6cd..269dd68 100644
--- a/Manual/Meta/Lean/Scopes.lean
+++ b/Manual/Meta/Lean/Scopes.lean
@@ -46,7 +46,8 @@ context to provide access to variables.
 -/
 def runWithVariables (elabFn : Array Expr → TermElabM α) : TermElabM α := do
   let scope := (← getScopes).head!
-  Term.withAutoBoundImplicit <|
+  Term.withAutoBoundImplicit do
+    let msgLog ← Core.getMessageLog
     Term.elabBinders scope.varDecls fun xs => do
       -- We need to synthesize postponed terms because this is a checkpoint for the auto-bound implicit feature
       -- If we don't use this checkpoint here, then auto-bound implicits in the postponed terms will not be handled correctly.
@@ -57,7 +58,7 @@ def runWithVariables (elabFn : Array Expr → TermElabM α) : TermElabM α := do
       withReader ({ · with sectionFVars := sectionFVars }) do
         -- We don't want to store messages produced when elaborating `(getVarDecls s)` because they have already been saved when we elaborated the `variable`(s) command.
         -- So, we use `Core.resetMessageLog`.
-        Core.resetMessageLog
+        Core.setMessageLog msgLog
         let someType := mkSort levelZero
         Term.addAutoBoundImplicits' xs someType fun xs _ =>
           Term.withoutAutoBoundImplicit <| elabFn xs
diff --git a/Manual/Monads.lean b/Manual/Monads.lean
index e82ccfa..817bc4f 100644
--- a/Manual/Monads.lean
+++ b/Manual/Monads.lean
@@ -64,7 +64,6 @@ The {name}`Alternative` type class describes applicative functors that additiona
 ```lean (show := false)
 section
 variable {α : Type u} {β : Type u}
-variable {n : Nat}
 ```
 
 ::::example "Lists with Lengths as Applicative Functors"
@@ -113,7 +112,7 @@ instance : Applicative (LenList n) where
     list := List.replicate n x
     lengthOk := List.length_replicate _ _
   }
-  seq fs xs := fs.zipWith (· ·) (xs ())
+  seq {α β} fs xs := fs.zipWith (· ·) (xs ())
 ```
 
 The well-behaved {name}`Monad` instance takes the diagonal of the results of applying the function:
@@ -128,7 +127,8 @@ def LenList.diagonal (square : LenList n (LenList n α)) : LenList n α :=
   match n with
   | 0 => ⟨[], rfl⟩
   | n' + 1 => {
-    list := square.head.head :: (square.tail.map (·.tail)).diagonal.list,
+    list :=
+      square.head.head :: (square.tail.map (·.tail)).diagonal.list
     lengthOk := by simp
   }
 ```
diff --git a/Manual/Monads/Laws.lean b/Manual/Monads/Laws.lean
index 26ee47a..de8b550 100644
--- a/Manual/Monads/Laws.lean
+++ b/Manual/Monads/Laws.lean
@@ -24,6 +24,8 @@ set_option linter.unusedVariables false
 tag := "monad-laws"
 %%%
 
+:::keepEnv
+
 ```lean (show := false)
 section Laws
 universe u u' v
@@ -38,7 +40,7 @@ axiom γ : Type u'
 axiom x : f α
 ```
 
-:::keepEnv
+
 ```lean (show := false)
 section F
 variable {f : Type u → Type v} [Functor f] {α β : Type u} {g : α → β} {h : β → γ} {x : f α}
@@ -64,7 +66,7 @@ The {name}`LawfulFunctor` class includes the necessary proofs.
 ```lean (show := false)
 end F
 ```
-:::
+
 
 In addition to proving that the potentially-optimized {name}`SeqLeft.seqLeft` and {name}`SeqRight.seqRight` operations are equivalent to their default implementations, Applicative functors {lean}`f` must satisfy four laws.
 
@@ -75,3 +77,5 @@ The {deftech}[monad laws] specify that {name}`pure` followed by {name}`bind` sho
 {docstring LawfulMonad}
 
 {docstring LawfulMonad.mk'}
+
+:::
diff --git a/Manual/Monads/Lift.lean b/Manual/Monads/Lift.lean
index 0efe0b3..95231b5 100644
--- a/Manual/Monads/Lift.lean
+++ b/Manual/Monads/Lift.lean
@@ -43,6 +43,11 @@ Users should not define new instances of {name}`MonadLiftT`, but it is useful as
 
 {docstring MonadLiftT}
 
+```lean (show := false)
+section
+variable {m : Type → Type u}
+```
+
 :::example "Monad Lifts in Function Signatures"
 The function {name}`IO.withStdin` has the following signature:
 ```signature
@@ -55,6 +60,10 @@ Because it doesn't require its parameter to precisely be in {name}`IO`, it can b
 The instance implicit parameter {lean}`MonadLiftT BaseIO m` allows the reflexive transitive closure of {name}`MonadLift` to be used to assemble the lift.
 :::
 
+```lean (show := false)
+end
+```
+
 
 When a term of type {lean}`n β` is expected, but the provided term has type {lean}`m α`, and the two types are not definitionally equal, Lean attempts to insert lifts and coercions before reporting an error.
 There are the following possibilities:
@@ -113,23 +122,31 @@ fun {α} act => liftM act : {α : Type} → BaseIO α → EIO IO.Error α
 There are also instances of {name}`MonadLift` for most of the standard library's {tech}[monad transformers], so base monad actions can be used in transformed monads without additional work.
 For example, state monad actions can be lifted across reader and exception transformers, allowing compatible monads to be intermixed freely:
 ````lean (keep := false)
-def incrBy (n : Nat) : StateM Nat Unit := modify (+ n)
+def incrBy (n : Nat) : StateM Nat Unit := modify (· + n)
 
 def incrOrFail : ReaderT Nat (ExceptT String (StateM Nat)) Unit := do
   if (← read) > 5 then throw "Too much!"
   incrBy (← read)
 ````
 
-Disabling lifting causes the code to fail to work:
-````lean (name := noLift)
+Disabling lifting causes an error:
+````lean (name := noLift) (error := true)
 set_option autoLift false
 
-def incrBy (n : Nat) : StateM Nat Unit := modify (+ n)
+def incrBy (n : Nat) : StateM Nat Unit := modify (. + n)
 
 def incrOrFail : ReaderT Nat (ExceptT String (StateM Nat)) Unit := do
   if (← read) > 5 then throw "Too much!"
   incrBy (← read)
 ````
+```leanOutput noLift
+type mismatch
+  incrBy __do_lift✝
+has type
+  StateM Nat Unit : Type
+but is expected to have type
+  ReaderT Nat (ExceptT String (StateM Nat)) Unit : Type
+```
 
 ::::
 :::::
diff --git a/Manual/Monads/Syntax.lean b/Manual/Monads/Syntax.lean
index 7ecd510..bbdb68e 100644
--- a/Manual/Monads/Syntax.lean
+++ b/Manual/Monads/Syntax.lean
@@ -20,6 +20,8 @@ set_option pp.rawOnError true
 set_option linter.unusedVariables false
 -- set_option trace.SubVerso.Highlighting.Code true
 
+set_option guard_msgs.diff true
+
 #doc (Manual) "Syntax" =>
 
 Lean supports programming with functors, applicative functors, and monads via special syntax:
@@ -589,7 +591,7 @@ p : α → Prop
 inst✝ : DecidablePred p
 xs : Array α
 out✝ : Array Nat := #[]
-col✝ : Std.Range := { start := 0, stop := xs.size, step := 1 }
+col✝ : Std.Range := { start := 0, stop := xs.size, step := 1, step_pos := Nat.zero_lt_one }
 i : Nat
 r✝ : Array Nat
 out : Array Nat := r✝
diff --git a/Manual/Monads/Zoo.lean b/Manual/Monads/Zoo.lean
index 43c6405..cfa9731 100644
--- a/Manual/Monads/Zoo.lean
+++ b/Manual/Monads/Zoo.lean
@@ -225,7 +225,7 @@ The standard library exports a mix of operations from the `-Of` and undecorated
 ```lean (show := false)
 example : @get = @MonadState.get := by rfl
 example : @set = @MonadStateOf.set := by rfl
-example (f : σ → σ) : @modify σ m inst f = @MonadState.modifyGet σ m inst PUnit fun (s : σ) => (PUnit.unit, f s) := by rfl
+example {inst} (f : σ → σ) : @modify σ m inst f = @MonadState.modifyGet σ m inst PUnit fun (s : σ) => (PUnit.unit, f s) := by rfl
 example : @modifyGet = @MonadState.modifyGet := by rfl
 example : @read = @MonadReader.read := by rfl
 example : @readThe = @MonadReaderOf.read := by rfl
diff --git a/Manual/NotationsMacros.lean b/Manual/NotationsMacros.lean
index c42ec23..f8f4ead 100644
--- a/Manual/NotationsMacros.lean
+++ b/Manual/NotationsMacros.lean
@@ -520,8 +520,8 @@ def ex2 (e) := show m _ from `(2 + $e :num)
 end
 ```
 
-::::keepEnv
-:::example "Expanding Quasiquotation"
+:::::keepEnv
+::::example "Expanding Quasiquotation"
 Printing the definition of {name}`f` demonstrates the expansion of a quasiquotation.
 ```lean (name := expansion)
 open Lean in
@@ -548,8 +548,11 @@ fun {m} [Monad m] [Lean.MonadQuotation m] x n => do
                   (Syntax.ident info "k".toSubstring' (Lean.addMacroScope mainModule `k scp) []))) }.raw
 ```
 
+:::paragraph
 ```lean (show := false)
 section
+open Lean (Term)
+open Lean.Quote
 variable {x : Term} {n : Nat}
 ```
 
@@ -558,13 +561,15 @@ It begins by constructing the source information for the resulting syntax, obtai
 It then obtains the current macro scope and the name of the module being processed, because macro scopes are added with respect to a module to enable independent compilation and avoid the need for a global counter.
 It then constructs a node using helpers such as {name}`Syntax.node1` and {name}`Syntax.node2`, which create a {name}`Syntax.node` with the indicated number of children.
 The macro scope is added to each identifier, and {name Lean.TSyntax.raw}`TSyntax.raw` is used to extract the contents of typed syntax wrappers.
-The antiquotations of {lean}`x` and {lean}`quote (n + 2)` occur directly in the expansion, as parameters to {name}`Syntax.node3`.
+The antiquotations of {lean}`x` and {lean type:="Term"}`quote (n + 2)` occur directly in the expansion, as parameters to {name}`Syntax.node3`.
 
 ```lean (show := false)
 end
 ```
 :::
+
 ::::
+:::::
 
 
 ### Splices
@@ -696,14 +701,14 @@ syntax "⟨| " (term)? " |⟩": term
 
 The `?` splice suffix for a term expects an {lean}`Option Term`:
 ```lean
-def mkStx [Monad m] [MonadQuotation m] (e) : m Term :=
+def mkStx [Monad m] [MonadQuotation m] (e : Option Term) : m Term :=
   `(⟨| $(e)? |⟩)
 ```
 ```lean (name := checkMkStx)
 #check mkStx
 ```
 ```leanOutput checkMkStx
-mkStx {m : Type → Type} [Monad m] [MonadQuotation m] (e : Option (TSyntax `term)) : m Term
+mkStx {m : Type → Type} [Monad m] [MonadQuotation m] (e : Option Term) : m Term
 ```
 
 Supplying {name}`some` results in the optional term being present.
@@ -716,7 +721,7 @@ Supplying {name}`some` results in the optional term being present.
 
 Supplying {name}`none` results in the optional term being absent.
 ```lean (name := noneMkStx)
-#eval do logInfo (← mkStx none))
+#eval do logInfo (← mkStx none)
 ```
 ```leanOutput noneMkStx
 ⟨| |⟩
@@ -970,7 +975,7 @@ open Lean.Macro
 The `arbitrary!` macro is intended to expand to some arbitrarily-determined value of a given type.
 
 ```lean
-syntax (name := arbitrary!) "arbitrary!" term:arg : term
+syntax (name := arbitrary!) "arbitrary! " term:arg : term
 ```
 
 :::keepEnv
@@ -1024,30 +1029,30 @@ macro_rules
 Additionally, if any rule throws the {name Lean.Macro.Exception.unsupportedSyntax}`unsupportedSyntax` exception, no further rules in that command are checked.
 ```lean
 macro_rules
-  | `(arbitrary! Nat) => throwUnsupported
-  | `(arbitrary! Nat) => `(42)
+  | `(arbitrary! (List Nat)) => throwUnsupported
+  | `(arbitrary! (List $_)) => `([])
 
 macro_rules
-  | `(arbitrary! Int) => `(42)
+  | `(arbitrary! (Array Nat)) => `(#[42])
 macro_rules
-  | `(arbitrary! Int) => throwUnsupported
+  | `(arbitrary! (Array $_)) => throwUnsupported
 ```
 
-The case for {lean}`Nat` fails to elaborate, because macro expansion did not translate the {keywordOf arbitrary!}`arbitrary!` syntax into something supported by the elaborator.
+The case for {lean}`List Nat` fails to elaborate, because macro expansion did not translate the {keywordOf arbitrary!}`arbitrary!` syntax into something supported by the elaborator.
 ```lean (name := arb3) (error := true)
-#eval arbitrary! Nat
+#eval arbitrary! (List Nat)
 ```
 ```leanOutput arb3
 elaboration function for 'arbitrary!' has not been implemented
-  arbitrary! Nat
+  arbitrary! (List Nat)
 ```
 
-The case for {lean}`Int` succeeds, because the first set of macro rules are attempted after the second throws the exception.
+The case for {lean}`Array Nat` succeeds, because the first set of macro rules are attempted after the second throws the exception.
 ```lean (name := arb4)
-#eval arbitrary! Int
+#eval arbitrary! (Array Nat)
 ```
 ```leanOutput arb4
-42
+#[42]
 ```
 ::::
 
diff --git a/Manual/RecursiveDefs/Structural.lean b/Manual/RecursiveDefs/Structural.lean
index 956a3a0..fdca950 100644
--- a/Manual/RecursiveDefs/Structural.lean
+++ b/Manual/RecursiveDefs/Structural.lean
@@ -328,7 +328,7 @@ Wrapping the discriminants in a pair breaks the connection.
 :::example "Structural Recursion Under Pairs"
 
 This function that finds the minimum of the two components of a pair can't be elaborated via structural recursion.
-```lean (error := true) (name := minpair)
+```lean (error := true) (name := minpair) (keep := false)
 def min' (nk : Nat × Nat) : Nat :=
   match nk with
   | (0, _) => 0
@@ -346,7 +346,7 @@ This is because the parameter's type, {name}`Prod`, is not recursive.
 Thus, its constructor has no recursive parameters that can be exposed by pattern matching.
 
 This definition is accepted using {tech}[well-founded recursion], however:
-```lean (keep := false)
+```lean
 def min' (nk : Nat × Nat) : Nat :=
   match nk with
   | (0, _) => 0
diff --git a/Manual/RecursiveDefs/Structural/CourseOfValuesExample.lean b/Manual/RecursiveDefs/Structural/CourseOfValuesExample.lean
index e44fd85..415004f 100644
--- a/Manual/RecursiveDefs/Structural/CourseOfValuesExample.lean
+++ b/Manual/RecursiveDefs/Structural/CourseOfValuesExample.lean
@@ -41,22 +41,25 @@ inductive Tree (α : Type u) : Type u where
   | branch (left : Tree α) (val : α) (right : Tree α)
 ```
 
-It's corresponding course-of-values table contains the realizations of the motive for all subtrees:
+Its corresponding course-of-values table contains the realizations of the motive for all subtrees:
 ```lean
 def Tree.below' {α : Type u} {motive : Tree α → Sort u} :
     Tree α → Sort (max 1 u)
   | .leaf => PUnit
   | .branch left _val right =>
-    motive left ×' motive right ×'
-    left.below' (motive := motive) ×'
-    right.below' (motive := motive)
+    (motive left ×' left.below' (motive := motive)) ×'
+    (motive right ×' right.below' (motive := motive))
 ```
 
 ```lean (show := false)
 theorem Tree.below_eq_below' : @Tree.below = @Tree.below' := by
   funext α motive t
-  induction t <;> simp [Tree.below, below']
-  congr
+  induction t
+  next =>
+    simp [Tree.below, Tree.below']
+  next ihl ihr =>
+    simp [Tree.below, Tree.below', ihl, ihr]
+
 ```
 
 For both lists and trees, the `brecOn` operator expects just a single case, rather than one per constructor.
@@ -96,7 +99,7 @@ def Tree.brecOnTable {α : Type u}
   | .branch left val right =>
     let resLeft := left.brecOnTable (motive := motive) step
     let resRight := right.brecOnTable (motive := motive) step
-    let branchRes := ⟨resLeft.1, resRight.1, resLeft.2, resRight.2⟩
+    let branchRes := ⟨resLeft, resRight⟩
     let val := step (.branch left val right) branchRes
     ⟨val, branchRes⟩
 ```
@@ -149,9 +152,10 @@ info: fun motive x y z step =>
 /--
 info: fun motive x z step =>
   step ((Tree.leaf.branch x Tree.leaf).branch z Tree.leaf)
-    ⟨step (Tree.leaf.branch x Tree.leaf) ⟨step Tree.leaf PUnit.unit, step Tree.leaf PUnit.unit, PUnit.unit, PUnit.unit⟩,
-      step Tree.leaf PUnit.unit, ⟨step Tree.leaf PUnit.unit, step Tree.leaf PUnit.unit, PUnit.unit, PUnit.unit⟩,
-      PUnit.unit⟩
+    ⟨⟨step (Tree.leaf.branch x Tree.leaf)
+          ⟨⟨step Tree.leaf PUnit.unit, PUnit.unit⟩, step Tree.leaf PUnit.unit, PUnit.unit⟩,
+        ⟨step Tree.leaf PUnit.unit, PUnit.unit⟩, step Tree.leaf PUnit.unit, PUnit.unit⟩,
+      step Tree.leaf PUnit.unit, PUnit.unit⟩
 -/
 #guard_msgs in
 #reduce fun motive x z step => Tree.brecOn' (motive := motive) (.branch (.branch .leaf x .leaf) z .leaf) step
diff --git a/Manual/RecursiveDefs/WF.lean b/Manual/RecursiveDefs/WF.lean
index 15a121c..b8d5aff 100644
--- a/Manual/RecursiveDefs/WF.lean
+++ b/Manual/RecursiveDefs/WF.lean
@@ -370,10 +370,33 @@ def Tree.depth (t : Tree) : Nat :=
   | none => 0
 termination_by t
 decreasing_by
+  cases t
   decreasing_tactic
 ```
 
-Note that the proof goal after {keywordOf Lean.Parser.Command.declaration}`decreasing_by` now includes the assumption {lean}`c ∈ t.children`, which suffices for {tactic}`decreasing_tactic` to succeed.
+Note that the proof goal after {keywordOf Lean.Parser.Command.declaration}`decreasing_by` now includes the assumption {lean}`c ∈ t.children`.
+The initial goal, that {lean}`sizeOf c < sizeOf t.children`, can be simplified with the {tactic}`cases` tactic into one for which  {tactic}`decreasing_tactic` succeeds.
+
+```lean (keep := false) (show := false)
+/--
+error: failed to prove termination, possible solutions:
+  - Use `have`-expressions to prove the remaining goals
+  - Use `termination_by` to specify a different well-founded relation
+  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
+t c : Tree
+hc : c ∈ t.children
+⊢ sizeOf c < sizeOf t
+-/
+#guard_msgs in
+def Tree.depth (t : Tree) : Nat :=
+  let depths := t.children.attach.map (fun ⟨c, hc⟩ => Tree.depth c)
+  match depths.max? with
+  | some d => d+1
+  | none => 0
+termination_by t
+decreasing_by
+  decreasing_tactic
+```
 
 :::
 
diff --git a/Manual/Terms.lean b/Manual/Terms.lean
index eca4938..84804b5 100644
--- a/Manual/Terms.lean
+++ b/Manual/Terms.lean
@@ -17,6 +17,7 @@ set_option linter.unusedVariables false
 open Lean.Elab.Tactic.GuardMsgs.WhitespaceMode
 
 set_option linter.constructorNameAsVariable false
+set_option guard_msgs.diff true
 
 #doc (Manual) "Terms" =>
 %%%
@@ -190,11 +191,11 @@ Even though `A` was opened more recently than the declaration of {name}`B.x`, th
 :::
 ::::
 
-::::keepEnv
+
 :::example "Ambiguous Identifiers"
 In this example, `x` could refer either to {name}`A.x` or {name}`B.x`, and neither takes precedence.
 Because both have the same type, it is an error.
-```lean (name := ambi)
+```lean (name := ambi) (error := true)
 def A.x := "A.x"
 def B.x := "B.x"
 open A
@@ -207,13 +208,11 @@ ambiguous, possible interpretations
 
   A.x : String
 ```
-```lean (show := false)
-```
 :::
-::::
-::::keepEnv
+
+
 :::example "Disambiguation via Typing"
-When they have different types, the types are used to disambiguate:
+When otherwise-ambiguous names have different types, the types are used to disambiguate:
 ```lean (name := ambiNo)
 def C.x := "C.x"
 def D.x := 3
@@ -225,7 +224,7 @@ open D
 "C.x"
 ```
 :::
-::::
+
 
 
 ## Leading `.`
@@ -870,7 +869,7 @@ axiom T.f : {n : Nat} → Char → T n → String
 
 Some functions are inconvenient to use with pipelines because their argument order is not conducive.
 For example, {name}`Array.push` takes an array as its first argument, not a {lean}`Nat`, leading to this error:
-```lean (name := arrPush)
+```lean (name := arrPush) (error := true)
 #eval #[1, 2, 3] |> Array.push 4
 ```
 ```leanOutput arrPush
@@ -1212,7 +1211,7 @@ They consist of the following:
 
 : Quoted names
 
-  Quoted names, such as {lean}`` `x `` and {lean}``` ``plus ```, match the corresponding {name}`Lean.Name` value.
+  Quoted names, such as {lean}`` `x `` and {lean}``` ``none ```, match the corresponding {name}`Lean.Name` value.
 
 : Macros
 
@@ -1385,7 +1384,7 @@ is not definitionally equal to the right-hand side
   3 = 5
 ⊢ 3 = 3 ∨ 3 = 5
 ---
-info: { val := 3, val2 := ?m.1487, ok := ⋯ } : OnlyThreeOrFive
+info: { val := 3, val2 := ?m.1542, ok := ⋯ } : OnlyThreeOrFive
 -/
 #guard_msgs in
 #check OnlyThreeOrFive.mk 3 ..
diff --git a/lake-manifest.json b/lake-manifest.json
index 67e602c..23e2225 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "bef462ba6d207757d877d1e4488ccd9dfa2c8409",
+   "rev": "9c0d4a38c4ed8850882a057c3073e936f5495470",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",