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

feat(library/blast): avoid default name when creating hypotheses

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-13 13:13:48 -08:00
parent bc8c5a3f68
commit 0dd6d6b140
2 changed files with 11 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/library/blast/intros.cpp
View file

@ -34,7 +34,12 @@ bool intros_action(unsigned max) {
for (unsigned i = 0; i < max; i++) {
if (!is_pi(target))
break;
expr href = s.mk_hypothesis(binding_name(target), binding_domain(target));
expr href;
if (is_default_var_name(binding_name(target)) && closed(binding_body(target))) {
href = s.mk_hypothesis(binding_domain(target));
} else {
href = s.mk_hypothesis(binding_name(target), binding_domain(target));
}
new_hs.push_back(href);
target = whnf(instantiate(binding_body(target), href));
}

7
src/library/blast/state.cpp
View file

@ -16,6 +16,7 @@ Author: Leonardo de Moura
namespace lean {
namespace blast {
static name * g_prefix = nullptr;
static name * g_H = nullptr;
bool metavar_decl::restrict_context_using(metavar_decl const & other) {
buffer<unsigned> to_erase;
@ -437,7 +438,7 @@ expr state::mk_hypothesis(name const & n, expr const & type, expr const & value)
expr state::mk_hypothesis(expr const & type, expr const & value) {
unsigned hidx = mk_href_idx();
return mk_hypothesis(hidx, name(*g_prefix, hidx), type, some_expr(value));
return mk_hypothesis(hidx, name(*g_H, hidx), type, some_expr(value));
}
expr state::mk_hypothesis(name const & n, expr const & type) {
@ -446,7 +447,7 @@ expr state::mk_hypothesis(name const & n, expr const & type) {
expr state::mk_hypothesis(expr const & type) {
unsigned hidx = mk_href_idx();
return mk_hypothesis(hidx, name(*g_prefix, hidx), type, none_expr());
return mk_hypothesis(hidx, name(*g_H, hidx), type, none_expr());
}
void state::del_hypotheses(buffer<hypothesis_idx> const & to_delete, hypothesis_idx_set const & to_delete_set) {
@ -694,9 +695,11 @@ expr state::mk_pi(list<expr> const & hrefs, expr const & b) const {
void initialize_state() {
g_prefix = new name(name::mk_internal_unique_name());
g_H = new name("H");
}
void finalize_state() {
delete g_prefix;
delete g_H;
}
}}