From ea6bf224e5af1dd9459ccb9d8ac4b15842c57f58 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 29 Jan 2014 15:22:37 -0800
Subject: [PATCH] feat(frontends/lean): make the parser accept (Type -> ...)

Before this commit, the parser would accept only a universe level or a ')' after '(' 'Type'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/parser_expr.cpp | 2 ++
 tests/lean/type0.lean              | 5 +++++
 tests/lean/type0.lean.expected.out | 7 +++++++
 3 files changed, 14 insertions(+)
 create mode 100644 tests/lean/type0.lean
 create mode 100644 tests/lean/type0.lean.expected.out

diff --git a/src/frontends/lean/parser_expr.cpp b/src/frontends/lean/parser_expr.cpp
index 54f219174..588897f21 100644
--- a/src/frontends/lean/parser_expr.cpp
+++ b/src/frontends/lean/parser_expr.cpp
@@ -823,6 +823,8 @@ expr parser_imp::parse_type(bool level_expected) {
     if (level_expected) {
         if (curr() == scanner::token::RightParen) {
             return save(Type(), p);
+        } else if (curr() == scanner::token::Arrow) {
+            return parse_arrow(save(Type(), p));
         } else {
             return save(mk_type(parse_level()), p);
         }
diff --git a/tests/lean/type0.lean b/tests/lean/type0.lean
new file mode 100644
index 000000000..08e67cde6
--- /dev/null
+++ b/tests/lean/type0.lean
@@ -0,0 +1,5 @@
+check (Type → Type)
+check (Type → Type) → Type
+check (Type 1)
+check ((Type 1) → Type) → Type
+check ((Type 1) → (Type 2)) → Type
\ No newline at end of file
diff --git a/tests/lean/type0.lean.expected.out b/tests/lean/type0.lean.expected.out
new file mode 100644
index 000000000..de70111c3
--- /dev/null
+++ b/tests/lean/type0.lean.expected.out
@@ -0,0 +1,7 @@
+  Set: pp::colors
+  Set: pp::unicode
+Type → Type : (Type 1)
+(Type → Type) → Type : (Type 1)
+(Type 1) : (Type 2)
+((Type 1) → Type) → Type : (Type 2)
+((Type 1) → (Type 2)) → Type : (Type 3)