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

refactor(library/rewriter): rename lc => ti

Browse source
This commit is contained in:
Soonho Kong 2013-12-01 01:57:34 -05:00
parent 506cca0ac1
commit 064e3fe20d
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/library/rewriter/rewriter.h
View file

@ -355,8 +355,8 @@ class apply_rewriter_fn {
std::pair<expr, expr> result; // m_rw(env, ctx, v);
// if (is_eqp(v, result.first))
type_inferer lc(env);
expr ty_v = lc(v, ctx);
type_inferer ti(env);
expr ty_v = ti(v, ctx);
switch (v.kind()) {
case expr_kind::Type:
@ -408,7 +408,7 @@ class apply_rewriter_fn {
result = rewrite_eq_rhs(env, ctx, v, result_rhs);
} else {
// nothing changed
result = std::make_pair(v, Refl(lc(v, ctx), v));
result = std::make_pair(v, Refl(ti(v, ctx), v));
}
}
std::pair<expr, expr> tmp = m_rw(env, ctx, result.first);
@ -439,7 +439,7 @@ class apply_rewriter_fn {
result = rewrite_lambda_body(env, ctx, v, result_body);
} else {
// nothing changed
result = std::make_pair(v, Refl(lc(v, ctx), v));
result = std::make_pair(v, Refl(ti(v, ctx), v));
}
}
std::pair<expr, expr> tmp = m_rw(env, ctx, result.first);
@ -471,7 +471,7 @@ class apply_rewriter_fn {
result = rewrite_pi_body(env, ctx, v, result_body);
} else {
// nothing changed
result = std::make_pair(v, Refl(lc(v, ctx), v));
result = std::make_pair(v, Refl(ti(v, ctx), v));
}
}
std::pair<expr, expr> tmp = m_rw(env, ctx, result.first);
@ -488,7 +488,7 @@ class apply_rewriter_fn {
expr const & body = let_body(v);
expr new_v = v;
expr ty_v = lc(v, ctx);
expr ty_v = ti(v, ctx);
expr pf = Refl(ty_v, v);
bool changed = false;