From ea910794fa2decb91e1f83e87ab37ffc38f9173f Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 16 Apr 2024 13:59:22 +0200 Subject: [PATCH] doc: crosslink {realize,resolve}GlobalName[NoOverload]?[WithInfo]?, (#3897) Co-authored-by: David Thrane Christiansen --- src/Lean/ReservedNameAction.lean | 6 ++++++ src/Lean/ResolveName.lean | 15 +++++++++++---- 2 files changed, 17 insertions(+), 4 deletions(-) diff --git a/src/Lean/ReservedNameAction.lean b/src/Lean/ReservedNameAction.lean index 6ce8346514..f0df67e74e 100644 --- a/src/Lean/ReservedNameAction.lean +++ b/src/Lean/ReservedNameAction.lean @@ -67,12 +67,18 @@ def realizeGlobalConstNoOverloadCore (n : Name) : CoreM Name := do /-- Similar to `resolveGlobalConst`, but also executes reserved name actions. + +Consider using `realizeGlobalConstWithInfo` if you want the syntax to show the resulting name's info +on hover. -/ def realizeGlobalConst (stx : Syntax) : CoreM (List Name) := withRef stx do preprocessSyntaxAndResolve stx realizeGlobalConstCore /-- Similar to `realizeGlobalConstNoOverload`, but also executes reserved name actions. + +Consider using `realizeGlobalConstNoOverloadWithInfo` if you want the syntax to show the resulting +name's info on hover. -/ def realizeGlobalConstNoOverload (id : Syntax) : CoreM Name := do ensureNonAmbiguous id (← realizeGlobalConst id) diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean index 05d016f25f..34c800fb48 100644 --- a/src/Lean/ResolveName.lean +++ b/src/Lean/ResolveName.lean @@ -289,7 +289,7 @@ def filterFieldList [Monad m] [MonadError m] (n : Name) (cs : List (Name × List if cs.isEmpty then throwUnknownConstant n return cs.map (·.1) -/-- Given a name `n`, return a list of possible interpretations for global constants. +/-- Given a name `n`, returns a list of possible interpretations for global constants. Similar to `resolveGlobalName`, but discard any candidate whose `fieldList` is not empty. For identifiers taken from syntax, use `resolveGlobalConst` instead, which respects preresolved names. -/ @@ -320,11 +320,14 @@ def preprocessSyntaxAndResolve [Monad m] [MonadResolveName m] [MonadEnv m] [Mona | _ => throwErrorAt stx s!"expected identifier" /-- -Interpret the syntax `n` as an identifier for a global constant, and return a list of resolved +Interprets the syntax `n` as an identifier for a global constant, and returns a list of resolved constant names that it could be referring to based on the currently open namespaces. This should be used instead of `resolveGlobalConstCore` for identifiers taken from syntax because `Syntax` objects may have names that have already been resolved. +Consider using `realizeGlobalConst` if you need to handle reserved names, and +`realizeGlobalConstWithInfo` if you want the syntax to show the resulting name's info on hover. + ## Example: ``` def Boo.x := 1 @@ -345,7 +348,7 @@ def resolveGlobalConst [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m preprocessSyntaxAndResolve stx resolveGlobalConstCore /-- -Given a list of names produced by `resolveGlobalConst`, throw an error if the list does not contain +Given a list of names produced by `resolveGlobalConst`, throws an error if the list does not contain exactly one element. Recall that `resolveGlobalConst` does not return empty lists. -/ @@ -355,9 +358,13 @@ def ensureNonAmbiguous [Monad m] [MonadError m] (id : Syntax) (cs : List Name) : | [c] => pure c | _ => throwErrorAt id s!"ambiguous identifier '{id}', possible interpretations: {cs.map mkConst}" -/-- Interpret the syntax `n` as an identifier for a global constant, and return a resolved +/-- Interprets the syntax `n` as an identifier for a global constant, and return a resolved constant name. If there are multiple possible interpretations it will throw. +Consider using `realizeGlobalConstNoOverload` if you need to handle reserved names, and +`realizeGlobalConstNoOverloadWithInfo` if you +want the syntax to show the resulting name's info on hover. + ## Example: ``` def Boo.x := 1