From cefbc277205d0e7a5e3e2243a9efeb491ef1535d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 24 Jun 2020 18:34:23 -0700 Subject: [PATCH] feat: add `elab` and `elab_rules` command syntax --- src/Lean/Parser/Syntax.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean index 00469e84d1..89fe0980e4 100644 --- a/src/Lean/Parser/Syntax.lean +++ b/src/Lean/Parser/Syntax.lean @@ -77,6 +77,12 @@ def macroTailDefault : Parser := try (" : " >> ident) >> darrow >> (("`(" >> ca def macroTail := macroTailTactic <|> macroTailCommand <|> macroTailDefault @[builtinCommandParser] def «macro» := parser! "macro " >> optPrecedence >> macroHead >> many macroArg >> macroTail +@[builtinCommandParser] def «elab_rules» := parser! "elab_rules" >> optKind >> optional (" : " >> ident) >> Term.matchAlts +def elabHead := macroHead +def elabArg := macroArg +def elabTail := try (" : " >> ident) >> darrow >> termParser +@[builtinCommandParser] def «elab» := parser! "elab " >> optPrecedence >> elabHead >> many elabArg >> elabTail + end Command end Parser