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

fix(library/aliases): aliases in sections and contexts

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-13 14:57:15 -08:00
parent 6e84696960
commit f0b002d5a7
2 changed files with 13 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/library/aliases.cpp
View file

@ -74,9 +74,8 @@ struct aliases_ext : public environment_extension {
void add_expr_alias_rec(name const & a, name const & e, bool overwrite = false) {
if (m_state.m_in_context) {
m_scopes = add_expr_alias_rec_core(m_scopes, a, e, overwrite);
} else {
add_expr_alias(a, e, overwrite);
}
add_expr_alias(a, e, overwrite);
}
void push(bool in_context) {
@ -107,7 +106,7 @@ struct aliases_ext : public environment_extension {
aliases_ext ext = get_extension(env);
ext.push(k != scope_kind::Namespace);
environment new_env = update(env, ext);
if (!::lean::in_context(new_env))
if (!::lean::in_context(new_env) && !::lean::in_section(new_env))
new_env = add_aliases(new_env, get_namespace(new_env), name());
return new_env;
}

11
tests/lean/run/private_names.lean Normal file
View file

@ -0,0 +1,11 @@
namespace bla
section
private definition foo : inhabited Prop :=
inhabited.mk false
instance [priority 1000] foo
example : inhabited.default Prop = false :=
rfl
end
end bla