From bda85f287c170479dce2975f1f5a28c861414391 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 2 Sep 2020 09:52:54 -0700 Subject: [PATCH] feat: `in` trailing command --- src/Lean/Parser/Command.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 39bb93d83d..b961814d06 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -97,6 +97,8 @@ def openSimple := parser! many1 ident @[builtinCommandParser] def «mutual» := parser! "mutual " >> many1 (notFollowedBy «end» >> commandParser) >> "end" +@[builtinCommandParser] def «in» := tparser! " in " >> commandParser + end Command end Parser end Lean