From 05cb45ca9c467b693eb3a39bb509bc1184f8325a Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 11 Aug 2020 16:50:29 +0200 Subject: [PATCH] refactor: simplify mkCategoryAntiquotParser --- src/Lean/Parser/Parser.lean | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/src/Lean/Parser/Parser.lean b/src/Lean/Parser/Parser.lean index b50cb62890..b65aacc256 100644 --- a/src/Lean/Parser/Parser.lean +++ b/src/Lean/Parser/Parser.lean @@ -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 =>