From ec1e6a68fa4a979bf2ca04357dad54af3272ed8a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 9 Dec 2020 17:35:16 -0800 Subject: [PATCH] feat: elaborate double quoted named literals --- src/Lean/Elab/Term.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 194ed651ee..f79f53a256 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -1290,12 +1290,16 @@ def elabScientificLit : TermElab := fun stx expectedType? => do | some val => return mkApp (Lean.mkConst `Char.ofNat) (mkNatLit val.toNat) | none => throwIllFormedSyntax -@[builtinTermElab quotedName] def elabQuotedName : TermElab := -fun stx _ => +@[builtinTermElab quotedName] def elabQuotedName : TermElab := fun stx _ => match stx[0].isNameLit? with | some val => pure $ toExpr val | none => throwIllFormedSyntax +@[builtinTermElab doubleQuotedName] def elabDoubleQuotedName : TermElab := fun stx _ => do + match stx[1].isNameLit? with + | some val => toExpr (← resolveGlobalConstNoOverload val) + | none => throwIllFormedSyntax + @[builtinTermElab typeOf] def elabTypeOf : TermElab := fun stx _ => do inferType (← elabTerm stx[1] none)