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)