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

feat(library/aliases): protected definitions in nested namespaces, closes #331

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-03 14:25:02 -08:00
parent 0443c1e70c
commit d10bb92a7d
2 changed files with 27 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/library/aliases.cpp
View file

@ -190,20 +190,20 @@ environment add_aliases(environment const & env, name const & prefix, name const
unsigned num_exceptions, name const * exceptions, bool overwrite) {
aliases_ext ext = get_extension(env);
env.for_each_declaration([&](declaration const & d) {
if (!is_protected(env, d.get_name()) &&
is_prefix_of(prefix, d.get_name()) && !is_exception(d.get_name(), prefix, num_exceptions, exceptions)) {
if (is_prefix_of(prefix, d.get_name()) && !is_exception(d.get_name(), prefix, num_exceptions, exceptions)) {
name a = d.get_name().replace_prefix(prefix, new_prefix);
if (!a.is_anonymous())
if (!(is_protected(env, d.get_name()) && a.is_atomic()) &&
!(a.is_anonymous()))
ext.add_expr_alias(a, d.get_name(), overwrite);
}
});
env.for_each_universe([&](name const & u) {
if (!is_protected(env, u) &&
is_prefix_of(prefix, u) && !is_exception(u, prefix, num_exceptions, exceptions)) {
if (is_prefix_of(prefix, u) && !is_exception(u, prefix, num_exceptions, exceptions)) {
name a = u.replace_prefix(prefix, new_prefix);
if (env.is_universe(a))
throw exception(sstream() << "universe level alias '" << a << "' shadows existing global universe level");
if (!a.is_anonymous())
if (!(is_protected(env, u) && a.is_atomic()) &&
!a.is_anonymous())
ext.add_level_alias(a, u);
}
});

21
tests/lean/run/331.lean Normal file
View file

@ -0,0 +1,21 @@
namespace nat
inductive less (a : nat) : nat → Prop :=
base : less a (succ a),
step : Π {b}, less a b → less a (succ b)
end nat
open nat
check less.rec_on
namespace foo1
protected definition foo2.bar := 10
end foo1
example : foo1.foo2.bar = 10 :=
rfl
open foo1
example : foo2.bar = 10 :=
rfl