diff --git a/src/Lean/Elab/Deriving/Basic.lean b/src/Lean/Elab/Deriving/Basic.lean
index fef6b74561..1522cc074f 100644
--- a/src/Lean/Elab/Deriving/Basic.lean
+++ b/src/Lean/Elab/Deriving/Basic.lean
@@ -14,6 +14,11 @@ def DerivingHandlerNoArgs := (typeNames : Array Name) → CommandElabM Bool
 
 builtin_initialize derivingHandlersRef : IO.Ref (NameMap DerivingHandler) ← IO.mkRef {}
 
+/-- A `DerivingHandler` is called on the fully qualified names of all types it is running for
+as well as the syntax of a `with` argument, if present.
+
+For example, `deriving instance Foo with fooArgs for Bar, Baz` invokes
+``fooHandler #[`Bar, `Baz] `(fooArgs)``. -/
 def registerBuiltinDerivingHandlerWithArgs (className : Name) (handler : DerivingHandler) : IO Unit := do
   unless (← initializing) do
     throw (IO.userError "failed to register deriving handler, it can only be registered during initialization")
@@ -21,6 +26,7 @@ def registerBuiltinDerivingHandlerWithArgs (className : Name) (handler : Derivin
     throw (IO.userError s!"failed to register deriving handler, a handler has already been registered for '{className}'")
   derivingHandlersRef.modify fun m => m.insert className handler
 
+/-- Like `registerBuiltinDerivingHandlerWithArgs` but ignoring any `with` argument. -/
 def registerBuiltinDerivingHandler (className : Name) (handler : DerivingHandlerNoArgs) : IO Unit := do
   registerBuiltinDerivingHandlerWithArgs className fun typeNames _ => handler typeNames
 
diff --git a/src/Lean/Elab/Deriving/Util.lean b/src/Lean/Elab/Deriving/Util.lean
index ebd07893b9..f5d07054af 100644
--- a/src/Lean/Elab/Deriving/Util.lean
+++ b/src/Lean/Elab/Deriving/Util.lean
@@ -13,9 +13,9 @@ def implicitBinderF := Parser.Term.implicitBinder
 def instBinderF     := Parser.Term.instBinder
 def explicitBinderF := Parser.Term.explicitBinder
 
-/-- Make fresh, hygienic names for every parameter and index of an inductive
-declaration. For example, `inductive Foo {α : Type} : Nat → Type` will give
-something like `#[α✝, a✝]`. -/
+/-- Make fresh, hygienic names for every parameter and index of an inductive declaration.
+
+For example, `inductive Foo {α : Type} : Nat → Type` will give something like ``#[`α✝, `a✝]``. -/
 def mkInductArgNames (indVal : InductiveVal) : TermElabM (Array Name) := do
   forallTelescopeReducing indVal.type fun xs _ => do
     let mut argNames := #[]
@@ -25,15 +25,25 @@ def mkInductArgNames (indVal : InductiveVal) : TermElabM (Array Name) := do
       argNames := argNames.push paramName
     pure argNames
 
+/-- Return the inductive declaration's type applied to the arguments in `argNames`. -/
 def mkInductiveApp (indVal : InductiveVal) (argNames : Array Name) : TermElabM Syntax :=
   let f    := mkIdent indVal.name
   let args := argNames.map mkIdent
   `(@$f $args*)
 
+/-- Return implicit binder syntaxes for the given `argNames`. The output matches `implicitBinder*`.
+
+For example, ``#[`foo,`bar]`` gives `` `({foo} {bar})``. -/
 def mkImplicitBinders (argNames : Array Name) : TermElabM (Array Syntax) :=
   argNames.mapM fun argName =>
     `(implicitBinderF| { $(mkIdent argName) })
 
+/-- Return instance binder syntaxes binding `className α` for every generic parameter `α`
+of the inductive `indVal` for which such a binding is type-correct. `argNames` is expected
+to provide names for the parameters (see `mkInductArgNames`). The output matches `instBinder*`.
+
+For example, given `inductive Foo {α : Type} (n : Nat) : (β : Type) → Type`, where `β` is an index,
+invoking ``mkInstImplicitBinders `BarClass foo #[`α, `n, `β]`` gives `` `([BarClass α])``. -/
 def mkInstImplicitBinders (className : Name) (indVal : InductiveVal) (argNames : Array Name) : TermElabM (Array Syntax) :=
   forallBoundedTelescope indVal.type indVal.numParams fun xs _ => do
     let mut binders := #[]