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

fix(library/init/lean/parser/command): add partial modifier

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-15 16:35:14 -07:00
parent b2e1ff8b3e
commit ee5ffb8ee2
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/init/lean/parser/command.lean
View file

@ -38,7 +38,8 @@ def «protected» := parser! "protected "
def visibility := «private» <|> «protected»
def «noncomputable» := parser! "noncomputable "
def «unsafe» := parser! "unsafe "
def declModifiers := parser! optional docComment >> optional «attributes» >> optional visibility >> optional «noncomputable» >> optional «unsafe»
def «partial» := parser! "partial "
def declModifiers := parser! optional docComment >> optional «attributes» >> optional visibility >> optional «noncomputable» >> optional «unsafe» >> optional «partial»
def declId := parser! ident >> optional (".{" >> sepBy1 ident ", " >> "}")
def declSig := parser! many Term.bracktedBinder >> Term.typeSpec
def optDeclSig := parser! many Term.bracktedBinder >> Term.optType