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

fix(frontends/lean): collect used universe levels after elaboration in the check command

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-08 13:36:00 -07:00
parent eab9321a3b
commit 57c85221fe
2 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/builtin_cmds.cpp
View file

@ -131,10 +131,10 @@ environment end_scoped_cmd(parser & p) {
static std::tuple<expr, level_param_names> parse_local_expr(parser & p) {
expr e = p.parse_expr();
list<expr> ctx = p.locals_to_context();
level_param_names ls = to_level_param_names(collect_univ_params(e));
level_param_names new_ls;
std::tie(e, new_ls) = p.elaborate_relaxed(e, ctx);
return std::make_tuple(e, append(ls, new_ls));
level_param_names ls = to_level_param_names(collect_univ_params(e));
return std::make_tuple(e, ls);
}
environment check_cmd(parser & p) {

1
tests/lean/run/mor.lean
View file

@ -11,5 +11,6 @@ namespace morphism
parameter {ob : Type}
parameter {C : category ob}
variables {a b c d : ob} {h : mor c d} {g : mor b c} {f : mor a b}
check mor a b
end
end morphism