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

chore: where struct instance parser

Browse source 
The parser was modified to fix issue https://github.com/leanprover/lean4/issues/753

cc @tydeu
This commit is contained in:
Leonardo de Moura 2021-12-12 08:22:31 -08:00
parent 56bae17924
commit 99bd215dcb
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
Lake/DSL/Commands.lean
View file

@ -30,7 +30,7 @@ syntax packageDeclTyped :=
Term.typeSpec declValSimple
syntax packageDeclSpec :=
ident (Term.whereDecls <|> packageDeclTyped <|> packageDeclWithBinders)?
ident (Command.whereStructInst <|> packageDeclTyped <|> packageDeclWithBinders)?
scoped syntax (name := packageDecl)
(docComment)? "package " packageDeclSpec : command