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

fix(frontends/lean/decl_cmds): allow binders but no type in definitions

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-25 09:00:57 -07:00
parent c427c5bdc9
commit 5b6589709c
1 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/frontends/lean/decl_cmds.cpp
View file

@ -236,8 +236,12 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque) {
{ {
parser::param_universe_scope scope2(p); parser::param_universe_scope scope2(p);
lenv = p.parse_binders(ps); lenv = p.parse_binders(ps);
p.check_token_next(g_colon, "invalid declaration, ':' expected"); if (p.curr_is_token(g_colon)) {
type = p.parse_scoped_expr(ps, *lenv); 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"); p.check_token_next(g_assign, "invalid declaration, ':=' expected");
value = p.parse_scoped_expr(ps, *lenv); value = p.parse_scoped_expr(ps, *lenv);