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

chore: remove restriction on leading/trailing_parser macros

Browse source 
I don't think we quote any parsers right now
This commit is contained in:
Sebastian Ullrich 2022-03-18 17:04:39 +01:00
parent 7460878e05
commit 99464c352e
1 changed files with 2 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Elab/BuiltinNotation.lean
View file

@ -100,12 +100,10 @@ private def elabParserMacroAux (prec : Syntax) (e : Syntax) : TermElabM Syntax :
let (some declName) ← getDeclName?
| throwError "invalid `leading_parser` macro, it must be used in definitions"
match extractMacroScopes declName with
| { name := Name.str _ s _, scopes := scps, .. } =>
| { name := Name.str _ s _, .. } =>
let kind := quote declName
let s := quote s
-- if the parser decl is hidden by hygiene, it doesn't make sense to provide an antiquotation kind
let antiquotKind ← if scps == [] then `(some $kind) else `(none)
``(withAntiquot (mkAntiquot $s $antiquotKind) (leadingNode $kind $prec $e))
``(withAntiquot (mkAntiquot $s $kind) (leadingNode $kind $prec $e))
| _ => throwError "invalid `leading_parser` macro, unexpected declaration name"
@[builtinTermElab «leading_parser»] def elabLeadingParserMacro : TermElab :=