max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: crosslink {realize,resolve}GlobalName[NoOverload]?[WithInfo]?, (#3897)

Browse source 
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
This commit is contained in:
Joachim Breitner 2024-04-16 13:59:22 +02:00 • committed by GitHub
parent a8df7d9d5c
commit ea910794fa
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 17 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/ReservedNameAction.lean
View file

@ -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)

15
src/Lean/ResolveName.lean
View file

@ -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