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

feat: add elab and elab_rules command syntax

Browse source
This commit is contained in:
Leonardo de Moura 2020-06-24 18:34:23 -07:00
parent 6f8dbb4506
commit cefbc27720
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Parser/Syntax.lean
View file

@ -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