doc: various docstrings

src/Lean/Elab/Tactic/Basic.lean

@@ -365,6 +365,8 @@ def closeMainGoal (val : Expr) (checkUnassigned := true): TacticM Unit := do
     replaceMainGoal mvarIds
     pure a
 
+/-- Get the mvarid of the main goal, run the given `tactic`,
+then set the new goals to be the resulting goal list.-/
 @[inline] def liftMetaTactic (tactic : MVarId → MetaM (List MVarId)) : TacticM Unit :=
   liftMetaTacticAux fun mvarId => do
     let gs ← tactic mvarId

src/Lean/Elab/Tactic/Conv/Basic.lean

@@ -12,6 +12,8 @@ import Lean.Elab.Tactic.BuiltinTactic
 namespace Lean.Elab.Tactic.Conv
 open Meta
 
+/-- Given `lhs`, returns a pair of metavariables `(?rhs, ?newGoal)`
+where `?newGoal : lhs = ?rhs`.-/
 def mkConvGoalFor (lhs : Expr) : MetaM (Expr × Expr) := do
   let lhsType ← inferType lhs
   let rhs ← mkFreshExprMVar lhsType
@@ -25,6 +27,9 @@ def markAsConvGoal (mvarId : MVarId) : MetaM MVarId := do
     return mvarId -- it is already tagged as LHS goal
   replaceTargetDefEq mvarId (mkLHSGoal (← getMVarType mvarId))
 
+/-- Given `lhs`, runs the `conv` tactic with the goal `⊢ lhs = ?rhs`.
+`conv` should produce no remaining goals that are not solvable with refl.
+Returns a pair of instantiated expressions `(?rhs, ?p)` where `?p : lhs = ?rhs`. -/
 def convert (lhs : Expr) (conv : TacticM Unit) : TacticM (Expr × Expr) := do
   let (rhs, newGoal) ← mkConvGoalFor lhs
   let savedGoals ← getGoals

src/Lean/Elab/Tactic/Location.lean

@@ -8,9 +8,13 @@ import Lean.Elab.Tactic.ElabTerm
 
 namespace Lean.Elab.Tactic
 
+/-- Denotes a set of locations where a tactic should be applied for the main goal. See also `withLocation`. -/
 inductive Location where
-  | wildcard
-  | targets (hypotheses : Array Syntax) (type : Bool)
+  | /-- Apply the tactic everywhere. -/
+    wildcard
+  | /-- `hypotheses` are hypothesis names in the main goal that the tactic should be applied to.
+        If `type` is true, then the tactic should also be applied to the target type. -/
+    targets (hypotheses : Array Syntax) (type : Bool)
 
 /-
 Recall that
@@ -35,6 +39,9 @@ def expandOptLocation (stx : Syntax) : Location :=
 
 open Meta
 
+/-- Runs the given `atLocal` and `atTarget` methods on each of the locations selected by the given `loc`.
+If any of the selected tactic applications fail, it will call `failed` with the main goal mvar.
+ -/
 def withLocation (loc : Location) (atLocal : FVarId → TacticM Unit) (atTarget : TacticM Unit) (failed : MVarId → TacticM Unit) : TacticM Unit := do
   match loc with
   | Location.targets hyps type =>

src/Lean/Meta/MatchUtil.lean

@@ -19,6 +19,7 @@ namespace Lean.Meta
   | none => p? (← whnf e)
   | s    => return s
 
+/-- matches `e` with `lhs = rhs : α` and returns `(α, lhs, rhs)`. -/
 def matchEq? (e : Expr) : MetaM (Option (Expr × Expr × Expr)) :=
   matchHelper? e fun e => return Expr.eq? e
 

src/Lean/MetavarContext.lean

@@ -420,6 +420,12 @@ def hasAssignableMVar [Monad m] [MonadMCtx m] : Expr → m Bool
 def assignLevelMVar [MonadMCtx m] (mvarId : MVarId) (val : Level) : m Unit :=
   modifyMCtx fun m => { m with lAssignment := m.lAssignment.insert mvarId val, usedAssignment := true }
 
+/--
+  Add `mvarId := u` to the metavariable assignment.
+  This method does not check whether `mvarId` is already assigned, nor it checks whether
+  a cycle is being introduced.
+  This is a low-level API, and it is safer to use `isDefEq (mkLevelMVar mvarId) u`.
+-/
 def assignExprMVar [MonadMCtx m] (mvarId : MVarId) (val : Expr) : m Unit :=
   modifyMCtx fun m => { m with eAssignment := m.eAssignment.insert mvarId val, usedAssignment := true }