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

fix(frontends/lean/tactic_hint): failure when compiling lean terms into

Browse source 
tactics: mismatch on the number of universe parameters
This commit is contained in:
Leonardo de Moura 2014-09-17 14:34:41 -07:00
parent 8b76deb971
commit 9733401c20
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/tactic_hint.cpp
View file

@ -91,10 +91,14 @@ list<tactic_hint_entry> get_tactic_hints(environment const & env) {
expr parse_tactic_name(parser & p) {
auto pos = p.pos();
name pre_tac = p.check_constant_next("invalid tactic name, constant expected");
expr pre_tac_type = p.env().get(pre_tac).get_type();
auto decl = p.env().get(pre_tac);
expr pre_tac_type = decl.get_type();
if (!is_constant(pre_tac_type) || const_name(pre_tac_type) != name("tactic"))
throw parser_error(sstream() << "invalid tactic name, '" << pre_tac << "' is not a tactic", pos);
return mk_constant(pre_tac);
buffer<level> ls;
for (auto const & n : decl.get_univ_params())
ls.push_back(mk_meta_univ(n));
return mk_constant(pre_tac, to_list(ls.begin(), ls.end()));
}
static name g_lbracket("[");