doc: improve doc-string for Meta.getConst?

doc/examples/widgets.lean

@@ -111,8 +111,8 @@ def getType (params : GetTypeParams) : RequestM (RequestTask CodeWithInfos) :=
   withWaitFindSnapAtPos params.pos fun snap => do
     runTermElabM snap do
       let name ← resolveGlobalConstNoOverloadCore params.name
-      let some c ← Meta.getConst? name
-        | throwThe RequestError ⟨.invalidParams, s!"no constant named '{name}'"⟩
+      let c ← try getConstInfo name
+        catch _ => throwThe RequestError ⟨.invalidParams, s!"no constant named '{name}'"⟩
       Widget.ppExprTagged c.type
 
 /-!

src/Lean/Meta/Basic.lean

@@ -833,9 +833,9 @@ private def getDefInfoTemp (info : ConstantInfo) : MetaM (Option ConstantInfo) :
     else
       return none
 
-/-- Remark: we later define `getConst?` at `GetConst.lean` after we define `Instances.lean`.
+/-- Remark: we later define `getUnfoldableConst?` at `GetConst.lean` after we define `Instances.lean`.
    This method is only used to implement `isClassQuickConst?`.
-   It is very similar to `getConst?`, but it returns none when `TransparencyMode.instances` and
+   It is very similar to `getUnfoldableConst?`, but it returns none when `TransparencyMode.instances` and
    `constName` is an instance. This difference should be irrelevant for `isClassQuickConst?`. -/
 private def getConstTemp? (constName : Name) : MetaM (Option ConstantInfo) := do
   match (← getEnv).find? constName with

src/Lean/Meta/ExprDefEq.lean

@@ -1148,7 +1148,7 @@ private def processAssignment' (mvarApp : Expr) (v : Expr) : MetaM Bool := do
 private def isDeltaCandidate? (t : Expr) : MetaM (Option ConstantInfo) := do
   match t.getAppFn with
   | Expr.const c _ =>
-    match (← getConst? c) with
+    match (← getUnfoldableConst? c) with
     | r@(some info) => if info.hasValue then return r else return none
     | _             => return none
   | _ => pure none

src/Lean/Meta/GetUnfoldableConst.lean

@@ -26,14 +26,25 @@ def canUnfold (info : ConstantInfo) : MetaM Bool := do
   else
     canUnfoldDefault ctx.config info
 
-def getConst? (constName : Name) : MetaM (Option ConstantInfo) := do
+/--
+Look up a constant name, returning the `ConstantInfo`
+if it should be unfolded at the current reducibility settings,
+or `none` otherwise.
+
+This is part of the implementation of `whnf`.
+External users wanting to look up names should be using `Lean.getConstInfo`.
+-/
+def getUnfoldableConst? (constName : Name) : MetaM (Option ConstantInfo) := do
   match (← getEnv).find? constName with
   | some (info@(.thmInfo _))  => getTheoremInfo info
   | some (info@(.defnInfo _)) => if (← canUnfold info) then return info else return none
   | some info                 => return some info
   | none                      => throwUnknownConstant constName
 
-def getConstNoEx? (constName : Name) : MetaM (Option ConstantInfo) := do
+/--
+As with `getUnfoldableConst?` but return `none` instead of failing if the constant is not found.
+-/
+def getUnfoldableConstNoEx? (constName : Name) : MetaM (Option ConstantInfo) := do
   match (← getEnv).find? constName with
   | some (info@(.thmInfo _))  => getTheoremInfo info
   | some (info@(.defnInfo _)) => if (← canUnfold info) then return info else return none

src/Lean/Meta/WHNF.lean

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 import Lean.Structure
 import Lean.Util.Recognizers
-import Lean.Meta.GetConst
+import Lean.Meta.GetUnfoldableConst
 import Lean.Meta.FunInfo
 import Lean.Meta.Match.MatcherInfo
 import Lean.Meta.Match.MatchPatternAttr
@@ -62,7 +62,7 @@ def isAuxDef (constName : Name) : MetaM Bool := do
 @[inline] private def matchConstAux {α} (e : Expr) (failK : Unit → MetaM α) (k : ConstantInfo → List Level → MetaM α) : MetaM α :=
   match e with
   | Expr.const name lvls => do
-    let (some cinfo) ← getConst? name | failK ()
+    let (some cinfo) ← getUnfoldableConst? name | failK ()
     k cinfo lvls
   | _ => failK ()
 
@@ -71,7 +71,7 @@ def isAuxDef (constName : Name) : MetaM Bool := do
 -- ===========================
 
 private def getFirstCtor (d : Name) : MetaM (Option Name) := do
-  let some (ConstantInfo.inductInfo { ctors := ctor::_, ..}) ← getConstNoEx? d | pure none
+  let some (ConstantInfo.inductInfo { ctors := ctor::_, ..}) ← getUnfoldableConstNoEx? d | pure none
   return some ctor
 
 private def mkNullaryCtor (type : Expr) (nparams : Nat) : MetaM (Option Expr) := do
@@ -209,7 +209,7 @@ private def reduceQuotRec (recVal  : QuotVal) (recLvls : List Level) (recArgs :
       let major ← whnf major
       match major with
       | Expr.app (Expr.app (Expr.app (Expr.const majorFn _) _) _) majorArg => do
-        let some (ConstantInfo.quotInfo { kind := QuotKind.ctor, .. }) ← getConstNoEx? majorFn | failK ()
+        let some (ConstantInfo.quotInfo { kind := QuotKind.ctor, .. }) ← getUnfoldableConstNoEx? majorFn | failK ()
         let f := recArgs[argPos]!
         let r := mkApp f majorArg
         let recArity := majorPos + 1
@@ -272,7 +272,7 @@ mutual
         | .mvar mvarId => return some mvarId
         | _ => getStuckMVar? e
       | .const fName _ =>
-        match (← getConstNoEx? fName) with
+        match (← getUnfoldableConstNoEx? fName) with
         | some <| .recInfo recVal  => isRecStuck? recVal e.getAppArgs
         | some <| .quotInfo recVal => isQuotRecStuck? recVal e.getAppArgs
         | _  =>
@@ -720,7 +720,7 @@ mutual
       if smartUnfolding.get (← getOptions) && (← getEnv).contains (mkSmartUnfoldingNameFor declName) then
         return none
       else
-        let some cinfo ← getConstNoEx? declName | pure none
+        let some cinfo ← getUnfoldableConstNoEx? declName | pure none
         unless cinfo.hasValue do return none
         deltaDefinition cinfo lvls
           (fun _ => pure none)