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

chore(frontends/lean/elaborator): remove confusing assign_mvar method

Browse source
This commit is contained in:
Sebastian Ullrich 2018-02-01 14:40:08 +01:00 • committed by Leonardo de Moura
parent 040748419f
commit 6eeb90c8fb
2 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/elaborator.cpp
View file

@ -3600,7 +3600,7 @@ expr elaborator::get_default_numeral_type() {
void elaborator::synthesize_numeral_types() {
for (expr const & A : m_numeral_types) {
if (is_metavar(instantiate_mvars(A))) {
if (!assign_mvar(A, get_default_numeral_type()))
if (!is_def_eq(A, get_default_numeral_type()))
report_or_throw(elaborator_exception(A, "invalid numeral, failed to force numeral to be a nat"));
}
}

1
src/frontends/lean/elaborator.h
View file

@ -116,7 +116,6 @@ private:
expr try_to_pi(expr const & e) { return m_ctx.try_to_pi(e); }
bool is_def_eq(expr const & e1, expr const & e2);
bool try_is_def_eq(expr const & e1, expr const & e2);
bool assign_mvar(expr const & e1, expr const & e2) { lean_assert(is_metavar(e1)); return is_def_eq(e1, e2); }
bool is_uvar_assigned(level const & l) const { return m_ctx.is_assigned(l); }
bool is_mvar_assigned(expr const & e) const { return m_ctx.is_assigned(e); }