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

refactor: simplify mkCategoryAntiquotParser

Browse source
This commit is contained in:
Sebastian Ullrich 2020-08-11 16:50:29 +02:00 • committed by Leonardo de Moura
parent 91de25ab02
commit 05cb45ca9c
1 changed files with 2 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1862,12 +1862,8 @@ match (parserExtension.getState env).categories.find? catName with
| none => false
| some cat => cat.leadingIdentAsSymbol
private def catNameToString : Name → String
| Name.str Name.anonymous s _ => s
| n => n.toString
@[inline] def mkCategoryAntiquotParser (kind : Name) : Parser :=
mkAntiquot (catNameToString kind) none
def mkCategoryAntiquotParser (kind : Name) : Parser :=
mkAntiquot kind.toString none
def categoryParserFnImpl (catName : Name) : ParserFn :=
fun ctx s =>