max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(frontends/lean/lean_elaborator): pre_equations => preEquations

Browse source
This commit is contained in:
Leonardo de Moura 2019-03-21 11:15:19 -07:00
parent 6988a8e69a
commit c017686f70
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/lean_elaborator.cpp
View file

@ -107,7 +107,7 @@ struct resolve_names_fn : public replace_visitor {
virtual expr visit(expr const & e) override {
if (is_placeholder(e) || is_as_is(e) || is_emptyc_or_emptys(e) || is_as_atomic(e)) {
return e;
} else if (is_annotation(e, "pre_equations")) {
} else if (is_annotation(e, "preEquations")) {
return visit_pre_equations(e);
} else if (is_annotation(e, "preresolved")) {
expr e2 = unwrap_pos(e);
@ -268,14 +268,14 @@ static expr unpack_mutual_definition(parser & p, expr const & cmd, buffer<name>
prv_names.push_back(scope2.get_actual_name());
fn = mk_local(n, n, fn_type, mk_rec_info());
p.add_local(fn);
if (!is_annotation(val, "pre_equations")) {
if (!is_annotation(val, "preEquations")) {
val = resolve_names(p, val);
}
}
optional<expr> wf_tacs;
if (args.size() > 6)
wf_tacs = args[6];
if (is_annotation(val, "pre_equations")) {
if (is_annotation(val, "preEquations")) {
// TODO(Sebastian): this uses the wrong declaration name scope
val = resolve_names(p, val);
to_equations(val, eqns);