From 5b6589709cf12e1313395a48a0551faca8ac5d0b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 25 Jun 2014 09:00:57 -0700 Subject: [PATCH] fix(frontends/lean/decl_cmds): allow binders but no type in definitions Signed-off-by: Leonardo de Moura --- src/frontends/lean/decl_cmds.cpp | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 952aedad27..68c8491c1c 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -236,8 +236,12 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque) { { parser::param_universe_scope scope2(p); lenv = p.parse_binders(ps); - p.check_token_next(g_colon, "invalid declaration, ':' expected"); - type = p.parse_scoped_expr(ps, *lenv); + if (p.curr_is_token(g_colon)) { + p.next(); + type = p.parse_scoped_expr(ps, *lenv); + } else { + type = p.save_pos(mk_expr_placeholder(), p.pos()); + } } p.check_token_next(g_assign, "invalid declaration, ':=' expected"); value = p.parse_scoped_expr(ps, *lenv);