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

Remove dead code

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-03 12:28:14 -07:00
parent cce469119f
commit 0b8fa3b167
3 changed files with 0 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/kernel/normalize.cpp
View file

@ -174,18 +174,9 @@ public:
unsigned k = length(m_ctx);
return reify(normalize(e, stack(), k), k);
}
expr operator()(expr const & e, expr const & v) {
unsigned k = length(m_ctx);
stack s = extend(stack(), normalize(v, stack(), k));
return reify(normalize(e, s, k+1), k+1);
}
};
expr normalize(expr const & e, environment const & env, context const & ctx) {
return normalize_fn(env, ctx)(e);
}
expr normalize(expr const & e, environment const & env, context const & ctx, expr const & v) {
return normalize_fn(env, ctx)(e, v);
}
}

2
src/kernel/normalize.h
View file

@ -13,6 +13,4 @@ namespace lean {
class environment;
/** \brief Normalize e using the environment env and context ctx */
expr normalize(expr const & e, environment const & env, context const & ctx = context());
/** \brief Normalize e using the environment env, context ctx, and add v to "normalization stack" */
expr normalize(expr const & e, environment const & env, context const & ctx, expr const & v);
}

4
src/kernel/type_check.cpp
View file

@ -20,10 +20,6 @@ class infer_type_fn {
return ::lean::normalize(e, m_env, ctx);
}
expr normalize(expr const & e, context const & ctx, expr const & v) {
return ::lean::normalize(e, m_env, ctx, v);
}
expr lookup(context const & c, unsigned i) {
context const & def_c = ::lean::lookup(c, i);
lean_assert(length(c) >= length(def_c));