diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean
index df2f925819..47582e0850 100644
--- a/src/Lean/Meta/Check.lean
+++ b/src/Lean/Meta/Check.lean
@@ -183,10 +183,16 @@ where
       ensureType b
       check b
 
+/--
+Throw an exception if `e` is not type correct.
+-/
 def check (e : Expr) : MetaM Unit :=
   traceCtx `Meta.check do
     withTransparency TransparencyMode.all $ checkAux e
 
+/--
+Return true if `e` is type correct.
+-/
 def isTypeCorrect (e : Expr) : MetaM Bool := do
   try
     check e
diff --git a/src/Lean/Meta/KAbstract.lean b/src/Lean/Meta/KAbstract.lean
index 206183517f..aed457f853 100644
--- a/src/Lean/Meta/KAbstract.lean
+++ b/src/Lean/Meta/KAbstract.lean
@@ -9,7 +9,12 @@ import Lean.Meta.Basic
 
 namespace Lean.Meta
 
-def kabstract (e : Expr) (p : Expr) (occs : Occurrences := Occurrences.all) : MetaM Expr := do
+/--
+Abstract occurrences of `p` in `e`. We detect subterms equivalent to `p` using key-matching.
+That is, only perform `isDefEq` tests when the head symbol of substerm is equivalent to head symbol of `p`.
+By default, all occurrences are abstracted, but this behavior can be controlled using the `occs` parameter.
+-/
+def kabstract (e : Expr) (p : Expr) (occs : Occurrences := .all) : MetaM Expr := do
   let e ← instantiateMVars e
   if p.isFVar && occs == Occurrences.all then
     return e.abstract #[p] -- Easy case
@@ -19,13 +24,13 @@ def kabstract (e : Expr) (p : Expr) (occs : Occurrences := Occurrences.all) : Me
     let rec visit (e : Expr) (offset : Nat) : StateRefT Nat MetaM Expr := do
       let visitChildren : Unit → StateRefT Nat MetaM Expr := fun _ => do
         match e with
-        | Expr.app f a         => return e.updateApp! (← visit f offset) (← visit a offset)
-        | Expr.mdata _ b       => return e.updateMData! (← visit b offset)
-        | Expr.proj _ _ b      => return e.updateProj! (← visit b offset)
-        | Expr.letE _ t v b _  => return e.updateLet! (← visit t offset) (← visit v offset) (← visit b (offset+1))
-        | Expr.lam _ d b _     => return e.updateLambdaE! (← visit d offset) (← visit b (offset+1))
-        | Expr.forallE _ d b _ => return e.updateForallE! (← visit d offset) (← visit b (offset+1))
-        | e                    => return e
+        | .app f a         => return e.updateApp! (← visit f offset) (← visit a offset)
+        | .mdata _ b       => return e.updateMData! (← visit b offset)
+        | .proj _ _ b      => return e.updateProj! (← visit b offset)
+        | .letE _ t v b _  => return e.updateLet! (← visit t offset) (← visit v offset) (← visit b (offset+1))
+        | .lam _ d b _     => return e.updateLambdaE! (← visit d offset) (← visit b (offset+1))
+        | .forallE _ d b _ => return e.updateForallE! (← visit d offset) (← visit b (offset+1))
+        | e                => return e
       if e.hasLooseBVars then
         visitChildren ()
       else if e.toHeadIndex != pHeadIdx || e.headNumArgs != pNumArgs then
diff --git a/src/Lean/Meta/KExprMap.lean b/src/Lean/Meta/KExprMap.lean
index 770e723274..7c37abd29b 100644
--- a/src/Lean/Meta/KExprMap.lean
+++ b/src/Lean/Meta/KExprMap.lean
@@ -18,6 +18,7 @@ structure KExprMap (α : Type) where
   map : Std.PHashMap HeadIndex (Std.AssocList Expr α) := {}
   deriving Inhabited
 
+/-- Return `some v` if there is an entry `e ↦ v` in `m`. -/
 def KExprMap.find? (m : KExprMap α) (e : Expr) : MetaM (Option α) := do
   match m.map.find? e.toHeadIndex with
   | none => return none
@@ -36,6 +37,7 @@ private def updateList (ps : Std.AssocList Expr α) (e : Expr) (v : α) : MetaM
     else
       return Std.AssocList.cons e' v' (← updateList ps e v)
 
+/-- Insert `e ↦ v` into `m` -/
 def KExprMap.insert (m : KExprMap α) (e : Expr) (v : α) : MetaM (KExprMap α) :=
   let k := e.toHeadIndex
   match m.map.find? k with