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

feat(frontends/lean/class): allow many instances to provided with a single 'instance' command

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-07 14:41:14 -07:00
parent 6ceecf6a15
commit 10b0dfeb37
2 changed files with 33 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/frontends/lean/class.cpp
View file

@ -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) {

19
tests/lean/run/class6.lean Normal file
View file

@ -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)
:= _