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

chore(compiler/simp_pr1_rec): cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2016-04-28 17:40:34 -07:00
parent 0b3e23892b
commit 21daa18950
1 changed files with 1 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/compiler/simp_pr1_rec.cpp
View file

@ -15,7 +15,7 @@ Author: Leonardo de Moura
#include "compiler/util.h"
namespace lean {
class simp_pr1_rec_fn : public replace_visitor {
class simp_pr1_rec_fn : public replace_visitor_closed {
environment m_env;
type_checker m_tc;
@ -157,13 +157,6 @@ class simp_pr1_rec_fn : public replace_visitor {
return replace_visitor::visit_app(e);
}
virtual expr visit_binding(expr const & b) {
expr new_domain = visit(binding_domain(b));
expr l = mk_local(mk_fresh_name(), new_domain);
expr new_body = abstract_local(visit(instantiate(binding_body(b), l)), l);
return update_binding(b, new_domain, new_body);
}
public:
simp_pr1_rec_fn(environment const & env):m_env(env), m_tc(env) {}
};