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

feat(library/tactic/dsimplify): replace assigned metavariables

Browse source
This commit is contained in:
Leonardo de Moura 2017-04-02 12:49:29 -07:00
parent 6dbf53f195
commit a007c93280
2 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/tactic/dsimplify.cpp
View file

@ -113,6 +113,10 @@ expr dsimplify_core_fn::visit_app(expr const & e) {
return e;
}
expr dsimplify_core_fn::visit_meta(expr const & e) {
return m_ctx.instantiate_mvars(e);
}
void dsimplify_core_fn::inc_num_steps() {
m_num_steps++;
if (m_num_steps > m_max_steps)
@ -143,13 +147,15 @@ expr dsimplify_core_fn::visit(expr const & e) {
expr new_e;
switch (curr_e.kind()) {
case expr_kind::Local:
case expr_kind::Meta:
case expr_kind::Sort:
case expr_kind::Constant:
new_e = curr_e;
break;
case expr_kind::Var:
lean_unreachable();
case expr_kind::Meta:
new_e = visit_meta(curr_e);
break;
case expr_kind::Macro:
new_e = visit_macro(curr_e);
break;

1
src/library/tactic/dsimplify.h
View file

@ -28,6 +28,7 @@ protected:
expr visit_binding(expr const & e);
expr visit_let(expr const & e);
expr visit_app(expr const & e);
expr visit_meta(expr const & e);
void inc_num_steps();
expr visit(expr const & e);