docs: document defeq and type inference related functions

Lean4Lean/Inductive/Reduce.lean

@@ -17,6 +17,15 @@ def mkNullaryCtor (type : Expr) (nparams : Nat) : Option Expr :=
   let name ← getFirstCtor env dName
   return mkAppRange (.const name ls) 0 nparams args
 
+/--
+When `e` has the type of a K-like inductive, converts it into a constructor
+application.
+
+For instance if we have `e : Eq a a`, it is converted into `Eq.refl a` (which
+it is definitionally equal to by proof irrelevance). Note that the indices of
+`e`'s type must match those of the constructor application (for instance,
+`e : Eq a b` cannot be converted if `a` and `b` are not defeq).
+-/
 def toCtorWhenK (rval : RecursorVal) (e : Expr) : m Expr := do
   assert! rval.k
   let appType ← whnf (← inferType e)
@@ -27,6 +36,7 @@ def toCtorWhenK (rval : RecursorVal) (e : Expr) : m Expr := do
     for h : i in [rval.numParams:appTypeArgs.size] do
       if (appTypeArgs[i]'h.2).hasExprMVar then return e
   let some newCtorApp := mkNullaryCtor env appType rval.numParams | return e
+  -- check that the indices of types of `e` and `newCtorApp` match
   unless ← isDefEq appType (← inferType newCtorApp) do return e
   return newCtorApp
 
@@ -40,6 +50,14 @@ def expandEtaStruct (eType e : Expr) : Expr :=
     result := .app result (.proj I i e)
   pure result
 
+/--
+When `e` is of struct type, converts it into a constructor application using
+projections.
+
+For instance if we have `e : String`, it is converted into
+`String.mk (String.data e)` (which is definitionally equal to `e` by struct
+eta).
+-/
 def toCtorWhenStruct (inductName : Name) (e : Expr) : m Expr := do
   if !isStructureLike env inductName || (e.isConstructorApp?' env).isSome then
     return e
@@ -52,6 +70,16 @@ def getRecRuleFor (rval : RecursorVal) (major : Expr) : Option RecursorRule := d
   let .const fn _ := major.getAppFn | none
   rval.rules.find? (·.ctor == fn)
 
+/--
+Performs recursor reduction on `e` (returning `none` if not applicable).
+
+For recursor reduction to occur, `e` must be a recursor application where the
+major premise is either a complete constructor application or of a K- or
+structure-like inductive type (in which case it is converted into an equivalent
+constructor application). The reduction is done by applying the
+`RecursorRule.rhs` associated with the constructor to the parameters from the
+recursor application and the fields of the constructor application.
+-/
 def inductiveReduceRec [Monad m] (env : Environment) (e : Expr)
     (whnf : Expr → m Expr) (inferType : Expr → m Expr) (isDefEq : Expr → Expr → m Bool) :
     m (Option Expr) := do
@@ -71,7 +99,10 @@ def inductiveReduceRec [Monad m] (env : Environment) (e : Expr)
   if rule.nfields > majorArgs.size then return none
   if ls.length != info.levelParams.length then return none
   let mut rhs := rule.rhs.instantiateLevelParams info.levelParams ls
+  -- get parameters from recursor application (recursor rules don't need the indices,
+  -- as these are determined by the constructor and its parameters/fields)
   rhs := mkAppRange rhs 0 info.getFirstIndexIdx recArgs
+  -- get fields from constructor application
   rhs := mkAppRange rhs (majorArgs.size - rule.nfields) majorArgs.size majorArgs
   if majorIdx + 1 < recArgs.size then
     rhs := mkAppRange rhs (majorIdx + 1) recArgs.size recArgs

Lean4Lean/Instantiate.lean

@@ -2,6 +2,10 @@ import Lean.Expr
 
 namespace Lean
 
+/--
+Reduces an expression of the form (λ x₁ ... xₙ, x₁) a₁ ... aₙ aₙ₊₁ ... aₘ
+to aᵢ aₙ₊₁ ... aₘ.
+-/
 def Expr.cheapBetaReduce (e : Expr) : Expr := Id.run do
   if !e.isApp then return e
   let fn := e.getAppFn
@@ -18,7 +22,7 @@ def Expr.cheapBetaReduce (e : Expr) : Expr := Id.run do
   let rec loop i fn : Id Expr :=
     if i < args.size then
       match fn with
-      | .lam _ _ dom .. => loop (i + 1) dom
+      | .lam _ _ bod .. => loop (i + 1) bod
       | _ => cont i fn
     else cont i fn
   loop 0 fn

Lean4Lean/Level.lean

@@ -10,6 +10,9 @@ def forEach [Monad m] (l : Level) (f : Level → m Bool) : m Unit := do
   | .max l₁ l₂ | .imax l₁ l₂ => l₁.forEach f; l₂.forEach f
   | .zero | .param .. | .mvar .. => pure ()
 
+/--
+Returns `some n` if level parameter `n` appears in `l` and `n ∉ ps`.
+-/
 def getUndefParam (l : Level) (ps : List Name) : Option Name := Id.run do
   (·.2) <$> StateT.run (s := none) do
     l.forEach fun l => do

Lean4Lean/Quot.lean

@@ -71,14 +71,31 @@ def Environment.addQuot (env : Environment) : Except KernelException Environment
   let all_quot := (← read).mkForall #[a] <| .app β quotMk_a
   withLocalDecl `q quot_r .implicit fun q => do
   -- constant Quot.ind.{u} {α : Sort u} {r : α → α → Prop} {β : @Quot.{u} α r → Prop} :
-  --   (∀ a : α, β (@Quot.mk.{u} α r a)) → ∀ q : @Quot.{u} α r, β q */
+  --   (∀ a : α, β (@Quot.mk.{u} α r a)) → ∀ q : @Quot.{u} α r, β q
   let env := add env <| .quotInfo {
     name := ``Quot.ind, kind := .ind, levelParams := [`u]
     type := (← read).mkForall #[α, r, β] <|
       .forallE `mk all_quot ((← read).mkForall #[q] <| .app β q) .default
   }
   return markQuotInit env
 
+/--
+Reduces the head application of a quotient eliminator as follows:
+
+```
+Quot.lift.{u, v} {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) :
+  (∀ a b : α, r a b → f a = f b) → @Quot.{u} α r → β
+
+Quot.lift f h (Quot.mk r a) ... ⟶ f a ...
+```
+
+```
+Quot.ind.{u} {α : Sort u} {r : α → α → Prop} {β : @Quot.{u} α r → Prop} :
+  (∀ a : α, β (@Quot.mk.{u} α r a)) → ∀ q : @Quot.{u} α r, β q
+
+Quot.ind p (Quot.mk r a) ... ⟶ p a ...
+```
+-/
 def quotReduceRec [Monad m] (e : Expr) (whnf : Expr → m Expr) : m (Option Expr) := do
   let .const fn _ := e.getAppFn | return none
   let cont mkPos argPos := do