michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean/parser): allow the user to write (Type) without providing a level

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-25 20:17:36 -08:00
parent 9fb3ccb4c0
commit 6bc1537e25
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/parser_expr.cpp
View file

@ -801,7 +801,11 @@ expr parser_imp::parse_type(bool level_expected) {
auto p = pos(); auto p = pos();
next(); next();
if (level_expected) { if (level_expected) {
return save(mk_type(parse_level()), p); if (curr() == scanner::token::RightParen) {
return save(Type(), p);
} else {
return save(mk_type(parse_level()), p);
}
} else { } else {
return save(Type(), p); return save(Type(), p);
} }