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

feat: support visibility modifiers on syntax abbrevs (#10228)

Browse source 
Closes #10068
This commit is contained in:
Sebastian Ullrich 2025-09-03 09:53:29 +02:00 • committed by GitHub
parent 6d68aab56a
commit 2efbe4ac36
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Elab/Syntax.lean
View file

@ -429,11 +429,11 @@ def elabSyntax (stx : Syntax) : CommandElabM Name := do
discard <| elabSyntax stx
@[builtin_command_elab «syntaxAbbrev»] def elabSyntaxAbbrev : CommandElab := fun stx => do
let `($[$doc?:docComment]? syntax $declName:ident := $[$ps:stx]*) ← pure stx | throwUnsupportedSyntax
let `($[$doc?:docComment]? $[$vis?:visibility]? syntax $declName:ident := $[$ps:stx]*) ← pure stx | throwUnsupportedSyntax
-- TODO: nonatomic names
let (val, _) ← runTermElabM fun _ => Term.toParserDescr (mkNullNode ps) Name.anonymous
let stxNodeKind := (← getCurrNamespace) ++ declName.getId
let stx' ← `($[$doc?:docComment]? meta def $declName:ident : Lean.ParserDescr := ParserDescr.nodeWithAntiquot $(quote (toString declName.getId)) $(quote stxNodeKind) $val)
let stx' ← `($[$doc?:docComment]? $[$vis?:visibility]? meta def $declName:ident : Lean.ParserDescr := ParserDescr.nodeWithAntiquot $(quote (toString declName.getId)) $(quote stxNodeKind) $val)
withMacroExpansion stx stx' <| elabCommand stx'
def checkRuleKind (given expected : SyntaxNodeKind) : Bool :=

2
src/Lean/Parser/Syntax.lean
View file

@ -87,7 +87,7 @@ def notationItem := ppSpace >> withAntiquot (mkAntiquot "notationItem" decl_name
optional docComment >> optional Term.«attributes» >> Term.attrKind >>
"syntax " >> optPrecedence >> optNamedName >> optNamedPrio >> many1 (ppSpace >> syntaxParser argPrec) >> " : " >> ident
@[builtin_command_parser] def syntaxAbbrev := leading_parser
optional docComment >> "syntax " >> ident >> " := " >> many1 syntaxParser
optional docComment >> optional visibility >> "syntax " >> ident >> " := " >> many1 syntaxParser
def catBehaviorBoth := leading_parser nonReservedSymbol "both"
def catBehaviorSymbol := leading_parser nonReservedSymbol "symbol"
def catBehavior := optional (" (" >> nonReservedSymbol "behavior" >> " := " >> (catBehaviorBoth <|> catBehaviorSymbol) >> ")")