fix: respect preresolved names at resolveConst*#583
fix: respect preresolved names at resolveConst*#583leodemoura merged 2 commits intoleanprover:masterfrom
resolveConst*#583Conversation
|
@leodemoura While I think this is definitely the correct way to go, there's no hurry in reviewing or merging it |
src/Lean/Elab/BuiltinTerm.lean
Outdated
| @[builtinTermElab doubleQuotedName] def elabDoubleQuotedName : TermElab := fun stx _ => do | ||
| match stx[1].isNameLit? with | ||
| | some val => toExpr (← resolveGlobalConstNoOverloadWithInfo stx[1] val) | ||
| | some val => toExpr (← resolveGlobalConstNoOverloadCore val) -- TODO: restore info |
There was a problem hiding this comment.
@leodemoura I think (double) quoted names should not be literals but use the regular ident parser. Otherwise they will not work correctly when quoted since they currently lack the preresolved information. Is there any reason not to change their parser?
There was a problem hiding this comment.
I would need a context switch to answer this question. Could you please add comments here explaining the issue? It would also be useful to open a new issue with examples that do not work.
I am assuming this PR can be merged independently of this issue. That is, it is not introducing any new issue.
There was a problem hiding this comment.
With the current state of the PR we would lose go-to-definition on double-quoted names, so we might want to resolve the ident issue first. Opened #586.
This makes sure we can properly quote e.g. `deriving` clauses and avoids a suspicious `eraseMacroScopes` call (though not at `Elab.Syntax`, since categories do not have to be declaration names)
|
Added a straightforward fix for #586 that changes the syntax of double-quoted names, but not single quoted ones, after noticing that we do use the latter with non-idents such as |
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
* [x] depends on leanprover#583 The final section `/-! # units -/` has not been ported, because it still depends on some earlier files. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
This makes sure we can properly quote e.g.
derivingclauses and avoids a suspiciouseraseMacroScopescall (though not atElab.Syntax, since categories do not have to be declaration names)