From 03a361edf415264820eff62e8f650fa903831f4b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 20 Sep 2020 13:42:50 -0700 Subject: [PATCH] feat: add `initialize` command parser --- src/Lean/Parser/Command.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index bec2f52a88..8e041b9fe7 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -96,6 +96,7 @@ def openSimple := parser! many1 ident @[builtinCommandParser] def «open» := parser! "open " >> (openHiding <|> openRenaming <|> openOnly <|> openSimple) @[builtinCommandParser] def «mutual» := parser! "mutual " >> many1 (notFollowedBy «end» >> commandParser) >> "end" +@[builtinCommandParser] def «initialize» := parser! "initialize " >> optional (ident >> Term.typeSpec >> Term.leftArrow) >> termParser @[builtinCommandParser] def «in» := tparser! " in " >> commandParser