From 6bc1537e25b280f36689a7423959963d359cb3aa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 25 Jan 2014 20:17:36 -0800 Subject: [PATCH] feat(frontends/lean/parser): allow the user to write (Type) without providing a level Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser_expr.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/frontends/lean/parser_expr.cpp b/src/frontends/lean/parser_expr.cpp index 86e66015cb..e054de01b7 100644 --- a/src/frontends/lean/parser_expr.cpp +++ b/src/frontends/lean/parser_expr.cpp @@ -801,7 +801,11 @@ expr parser_imp::parse_type(bool level_expected) { auto p = pos(); next(); 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 { return save(Type(), p); }