diff --git a/Manual/Classes/InstanceDecls.lean b/Manual/Classes/InstanceDecls.lean
index 0697a82a..89969050 100644
--- a/Manual/Classes/InstanceDecls.lean
+++ b/Manual/Classes/InstanceDecls.lean
@@ -122,7 +122,7 @@ Instances for recursive inductive types are common, however.
 There is a standard idiom to work around this limitation: define a recursive function independently of the instance, and then refer to it in the instance definition.
 By convention, these recursive functions have the name of the corresponding method, but are defined in the type's namespace.
 
-::: example "Instances are not recursive"
+:::example "Instances are not recursive"
 Given this definition of {lean}`NatTree`:
 ```lean
 inductive NatTree where
@@ -153,7 +153,7 @@ def NatTree.beq : NatTree → NatTree → Bool
   | .leaf, .leaf =>
     true
   | .branch l1 v1 r1, .branch l2 v2 r2 =>
-    l1 == l2 && v1 == v2 && r1 == r2
+    NatTree.beq l1 l2 && v1 == v2 && NatTree.beq r1 r2
   | _, _ =>
     false
 ```
diff --git a/Manual/Meta/Example.lean b/Manual/Meta/Example.lean
index d91993eb..c4ee36c0 100644
--- a/Manual/Meta/Example.lean
+++ b/Manual/Meta/Example.lean
@@ -76,15 +76,15 @@ def getLeanBlockContents? : TSyntax `block → DocElabM (LeanBlockContent)
   | `(block|```$nameStx:ident $args*|$contents:str```) => do
     let name ← realizeGlobalConstNoOverload nameStx
     if name == ``Manual.imports then
-      return {content := some contents.getString, shouldElab := false}
+      return { content := some contents.getString, shouldElab := false }
     if name != ``Verso.Genre.Manual.InlineLean.lean then
-      return {content := none, shouldElab := false}
+      return { content := none, shouldElab := false }
     let args ← Verso.Doc.Elab.parseArgs args
     let args ← parseThe InlineLean.LeanBlockConfig args
     if !args.keep || args.error then
-      return {content := none, shouldElab := true}
-    pure <| {content := some contents.getString, shouldElab := true}
-  | _ => pure {content := none, shouldElab := false}
+      return { content := none, shouldElab := true }
+    pure <| { content := some contents.getString, shouldElab := true }
+  | _ => pure { content := none, shouldElab := false }
 
 /--
 Elaborates all Lean blocks first, enabling local forward references