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

feat: add prio parser category

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-14 13:13:58 -08:00
parent 35f9518559
commit 216d34e178
1 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -17,9 +17,16 @@ builtin_initialize
registerBuiltinParserAttribute `builtinPrecParser `prec (leadingIdentAsSymbol := true)
registerBuiltinDynamicParserAttribute `precParser `prec
builtin_initialize
registerBuiltinParserAttribute `builtinPrioParser `prio (leadingIdentAsSymbol := true)
registerBuiltinDynamicParserAttribute `prioParser `prio
@[inline] def precedenceParser (rbp : Nat := 0) : Parser :=
categoryParser `prec rbp
@[inline] def priorityParser (rbp : Nat := 0) : Parser :=
categoryParser `prio rbp
@[inline] def syntaxParser (rbp : Nat := 0) : Parser :=
categoryParser `stx rbp
@ -45,6 +52,7 @@ namespace Term
@[builtinTermParser] def stx.quot : Parser := parser! "`(stx|" >> toggleInsideQuot syntaxParser >> ")"
@[builtinTermParser] def prec.quot : Parser := parser! "`(prec|" >> toggleInsideQuot precedenceParser >> ")"
@[builtinTermParser] def prio.quot : Parser := parser! "`(prio|" >> toggleInsideQuot priorityParser >> ")"
end Term