From 10b0dfeb37b48c07c26aecdf2d5ca514dda72e1f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 7 Jul 2014 14:41:14 -0700 Subject: [PATCH] feat(frontends/lean/class): allow many instances to provided with a single 'instance' command Signed-off-by: Leonardo de Moura --- src/frontends/lean/class.cpp | 19 ++++++++++++++----- tests/lean/run/class6.lean | 19 +++++++++++++++++++ 2 files changed, 33 insertions(+), 5 deletions(-) create mode 100644 tests/lean/run/class6.lean diff --git a/src/frontends/lean/class.cpp b/src/frontends/lean/class.cpp index deb47b1400..b6c940d552 100644 --- a/src/frontends/lean/class.cpp +++ b/src/frontends/lean/class.cpp @@ -119,11 +119,20 @@ environment add_class_cmd(parser & p) { } environment add_instance_cmd(parser & p) { - auto pos = p.pos(); - name c = p.check_id_next("invalid 'class instance' declaration, identifier expected"); - expr e = p.id_to_expr(c, pos); - if (!is_constant(e)) throw parser_error(sstream() << "invalid 'class instance' declaration, '" << c << "' is not a constant", pos); - return add_instance(p.env(), const_name(e)); + bool found = false; + environment env = p.env(); + while (p.curr_is_identifier()) { + found = true; + auto pos = p.pos(); + name c = p.get_name_val(); + p.next(); + expr e = p.id_to_expr(c, pos); + if (!is_constant(e)) throw parser_error(sstream() << "invalid 'class instance' declaration, '" << c << "' is not a constant", pos); + env = add_instance(env, const_name(e)); + } + if (!found) + throw parser_error("invalid 'class instance' declaration, at least one identifier expected", p.pos()); + return env; } void register_class_cmds(cmd_table & r) { diff --git a/tests/lean/run/class6.lean b/tests/lean/run/class6.lean new file mode 100644 index 0000000000..eb73039e19 --- /dev/null +++ b/tests/lean/run/class6.lean @@ -0,0 +1,19 @@ +import standard + +inductive t1 : Type := +| mk1 : t1 + +inductive t2 : Type := +| mk2 : t2 + +theorem inhabited_t1 : inhabited t1 +:= inhabited_intro mk1 + +theorem inhabited_t2 : inhabited t2 +:= inhabited_intro mk2 + +instance inhabited_t1 inhabited_t2 + +theorem T : inhabited (t1 × t2) +:= _ +