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

feat: add initialize command parser

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-20 13:42:50 -07:00
parent 13abf0bd45
commit 03a361edf4
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Lean/Parser/Command.lean
View file

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