feat(library/scoped_ext): force user to end a scope with an identifier matching the one used in beginning of scope, closes #30

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

library/hott/logic.lean

@@ -16,7 +16,7 @@ definition transport {A : Type} {a b : A} {P : A → Type} (H1 : a = b) (H2 : P
 
 namespace logic
   notation p `*(`:75 u `)` := transport p u
-end
+end logic
 using logic
 
 definition symm {A : Type} {a b : A} (p : a = b) : b = a
@@ -32,7 +32,7 @@ calc_trans trans
 namespace logic
   postfix `⁻¹`:100 := symm
   infixr `⬝`:75 := trans
-end
+end logic
 using logic
 
 theorem trans_refl_right {A : Type} {x y : A} (p : x = y) : p = p ⬝ (refl y)
@@ -115,7 +115,7 @@ abbreviation homotopy {A : Type} {P : A → Type} (f g : Π x, P x)
 
 namespace logic
   infix `∼`:50 := homotopy
-end
+end logic
 using logic
 
 notation `assume` binders `,` r:(scoped f, f) := r
@@ -215,7 +215,7 @@ inductive sum (A : Type) (B : Type) : Type :=
 
 namespace logic
   infixr `+`:25 := sum
-end
+end logic
 using logic
 infixr `∨`:25 := sum
 

library/hott/num.lean

@@ -14,4 +14,4 @@ inductive pos_num : Type :=
 inductive num : Type :=
 | zero  : num
 | pos   : pos_num → num
-end
+end num

library/hott/string.lean

@@ -10,4 +10,4 @@ inductive char : Type :=
 inductive string : Type :=
 | empty : string
 | str   : char → string → string
-end
+end string

library/hott/tactic.lean

@@ -51,4 +51,4 @@ notation `?` t:max     := try t
 definition repeat1     (t : tactic) : tactic := t ; !t
 definition focus       (t : tactic) : tactic := focus_at t 0
 definition determ      (t : tactic) : tactic := at_most t 1
-end
+end tactic

library/standard/data/bool.lean

@@ -141,4 +141,4 @@ theorem bnot_false : !ff = tt := refl _
 
 theorem bnot_true  : !tt = ff := refl _
 
-end
+end bool

library/standard/data/nat/basic.lean

@@ -12,7 +12,7 @@ using decidable (hiding induction_on rec_on)
 namespace helper_tactics
   definition apply_refl := apply @refl
   tactic_hint apply_refl
-end
+end helper_tactics
 using helper_tactics
 
 

library/standard/data/nat/order.lean

@@ -583,7 +583,4 @@ mul_eq_one_left ((mul_comm n m) ▸ H)
 
 --- theorem mul_eq_one {n m : ℕ} (H : n * m = 1) : n = 1 ∧ m = 1
 --- := and_intro (mul_eq_one_left H) (mul_eq_one_right H)
-
+end nat
-opaque_hint (hiding lt)
-
-end -- namespace nat

library/standard/data/nat/sub.lean

@@ -508,6 +508,4 @@ or_elim (le_total k l)
   (assume H : k ≤ l, dist_comm l k ▸ dist_comm _ _ ▸ aux l k H)
   (assume H : l ≤ k, aux k l H)
 
-opaque_hint (hiding dist)
+end nat
-
-end -- namespace nat

library/standard/data/num.lean

@@ -26,4 +26,4 @@ inhabited_intro one
 theorem inhabited_num [instance] : inhabited num :=
 inhabited_intro zero
 
-end
+end num

library/standard/data/option.lean

@@ -45,4 +45,4 @@ rec_on o₁
     (take a₂ : A, decidable.rec_on (H a₁ a₂)
       (assume Heq : a₁ = a₂, inl (Heq ▸ refl _))
       (assume Hne : a₁ ≠ a₂, inr (assume Hn : some a₁ = some a₂, absurd (some_inj Hn) Hne))))
-end
+end option

library/standard/data/pair.lean

@@ -10,7 +10,7 @@ namespace pair
 inductive pair (A : Type) (B : Type) : Type :=
 | mk_pair : A → B → pair A B
 
-section
+section thms
   parameter {A : Type}
   parameter {B : Type}
 
@@ -34,7 +34,7 @@ section
        ... = mk_pair (fst p2) (snd p1) : {H1}
        ... = mk_pair (fst p2) (snd p2) : {H2}
        ... = p2                        : pair_ext p2
-end
+end thms
 
 instance pair_inhabited
 
@@ -43,4 +43,4 @@ infixr × := pair
 
 -- notation for n-ary tuples
 notation `(` h `,` t:(foldl `,` (e r, mk_pair r e) h) `)` := t
-end
+end pair

library/standard/data/set.lean

@@ -61,4 +61,4 @@ theorem union_assoc (A B C : set T) : (A ∪ B) ∪ C = A ∪ (B ∪ C) :=
 funext (λx, bor_assoc (A x) (B x) (C x))
 
 end
-end
+end set

library/standard/data/string.lean

@@ -21,4 +21,4 @@ inhabited_intro (ascii ff ff ff ff ff ff ff ff)
 theorem inhabited_string [instance] : inhabited string :=
 inhabited_intro empty
 
-end
+end string

library/standard/data/sum.lean

@@ -15,4 +15,4 @@ infixr `+`:25 := sum
 
 theorem induction_on {A : Type} {B : Type} {C : Prop} (s : A + B) (H1 : A → C) (H2 : B → C) : C :=
 sum_rec H1 H2 s
-end
+end sum

library/standard/data/unit.lean

@@ -21,4 +21,4 @@ inhabited_intro ⋆
 
 theorem decidable_eq [instance] (a b : unit) : decidable (a = b) :=
 inl (unit_eq a b)
-end
+end unit

library/standard/logic/axioms/funext.lean

@@ -24,4 +24,5 @@ section
 
   theorem compose_const_right (f : B → C) (b : B) : f ∘ (const A b) = const A (f b) :=
   funext (take x, refl _)
-end end
+end
+end function

library/standard/logic/classes/decidable.lean

@@ -87,4 +87,4 @@ rec_on Ha
 theorem decidable_eq_equiv {a b : Prop} (Ha : decidable a) (H : a = b) : decidable b :=
 decidable_iff_equiv Ha (eq_to_iff H)
 
-end
+end decidable

library/standard/logic/connectives/eq.lean

@@ -35,7 +35,7 @@ namespace eq_proofs
   postfix `⁻¹`:100 := symm
   infixr `⬝`:75     := trans
   infixr `▸`:75    := subst
-end
+end eq_proofs
 using eq_proofs
 
 theorem congr1 {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a :=

library/standard/logic/connectives/function.lean

@@ -52,4 +52,4 @@ notation f `-[` op `]-` g  := combine f op g
 -- Trick for using any binary function as infix operator
 notation a `⟨` f `⟩` b     :=  f a b
 
-end
+end function

library/standard/struc/binary.lean

@@ -36,4 +36,4 @@ section
       ...   = a*(c*b) : {H_comm _ _}
       ...   = (a*c)*b : (H_assoc _ _ _)⁻¹
 end
-end
+end binary

library/standard/struc/equivalence.lean

@@ -27,4 +27,5 @@ equivalence_rec (λ r s t, s) H
 
 theorem equivalence_transitive [instance] {A : Type} {p : A → A → Prop} (H : equivalence p) : transitive p :=
 equivalence_rec (λ r s t, t) H
-end
+
+end equivalence

library/standard/tools/tactic.lean

@@ -54,4 +54,4 @@ notation `?` t:max     := try t
 definition repeat1     (t : tactic) : tactic := t ; !t
 definition focus       (t : tactic) : tactic := focus_at t 0
 definition determ      (t : tactic) : tactic := at_most t 1
-end
+end tactic

src/frontends/lean/builtin_cmds.cpp

@@ -63,8 +63,11 @@ environment print_cmd(parser & p) {
 }
 
 environment section_cmd(parser & p) {
+    name n;
+    if (p.curr_is_identifier())
+        n = p.check_atomic_id_next("invalid section, atomic identifier expected");
     p.push_local_scope();
-    return push_scope(p.env(), p.ios());
+    return push_scope(p.env(), p.ios(), true, n);
 }
 
 environment namespace_cmd(parser & p) {
@@ -72,13 +75,18 @@ environment namespace_cmd(parser & p) {
     name n = p.check_atomic_id_next("invalid namespace declaration, atomic identifier expected");
     if (is_root_namespace(n))
         throw parser_error(sstream() << "invalid namespace name, '" << n << "' is reserved", pos);
-    return push_scope(p.env(), p.ios(), n);
+    return push_scope(p.env(), p.ios(), false, n);
 }
 
 environment end_scoped_cmd(parser & p) {
     if (in_section(p.env()))
         p.pop_local_scope();
-    return pop_scope(p.env());
+    if (p.curr_is_identifier()) {
+        name n = p.check_atomic_id_next("invalid end of scope, atomic identifier expected");
+        return pop_scope(p.env(), n);
+    } else {
+        return pop_scope(p.env());
+    }
 }
 
 environment check_cmd(parser & p) {

src/library/scoped_ext.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include <vector>
 #include <memory>
 #include <string>
+#include "util/sstream.h"
 #include "library/scoped_ext.h"
 #include "library/kernel_bindings.h"
 
@@ -26,9 +27,10 @@ void register_scoped_ext(name const & c, using_namespace_fn use, push_scope_fn p
 }
 
 struct scope_mng_ext : public environment_extension {
-    name_set   m_namespace_set; // all namespaces registered in the system
+    name_set     m_namespace_set; // all namespaces registered in the system
-    list<name> m_namespaces; // stack of namespaces/sections
+    list<name>   m_namespaces;    // stack of namespaces/sections
-    list<bool> m_in_section;
+    list<name>   m_headers;       // namespace/section header
+    list<bool>   m_in_section;
 };
 
 struct scope_mng_ext_reg {
@@ -80,10 +82,9 @@ optional<name> to_valid_namespace_name(environment const & env, name const & n)
 }
 
 static std::string g_new_namespace_key("nspace");
-environment push_scope(environment const & env, io_state const & ios, name const & n) {
+environment push_scope(environment const & env, io_state const & ios, bool add_sec, name const & n) {
-    if (!n.is_anonymous() && in_section(env))
+    if (!add_sec && in_section(env))
         throw exception("invalid namespace declaration, a namespace cannot be declared inside a section");
-    bool in_section = n.is_anonymous();
     name new_n = get_namespace(env) + n;
     scope_mng_ext ext = get_extension(env);
     bool save_ns = false;
@@ -92,12 +93,13 @@ environment push_scope(environment const & env, io_state const & ios, name const
         ext.m_namespace_set.insert(new_n);
     }
     ext.m_namespaces = cons(new_n, ext.m_namespaces);
-    ext.m_in_section = cons(n.is_anonymous(), ext.m_in_section);
+    ext.m_headers    = cons(n, ext.m_headers);
+    ext.m_in_section = cons(add_sec, ext.m_in_section);
     environment r = update(env, ext);
     for (auto const & t : get_exts()) {
-        r = std::get<2>(t)(r, in_section);
+        r = std::get<2>(t)(r, add_sec);
     }
-    if (!n.is_anonymous())
+    if (!add_sec)
         r = using_namespace(r, ios, n);
     if (save_ns)
         r = module::add(r, g_new_namespace_key, [=](serializer & s) { s << new_n; });
@@ -117,12 +119,15 @@ static void namespace_reader(deserializer & d, module_idx, shared_environment &,
 }
 register_module_object_reader_fn g_namespace_reader(g_new_namespace_key, namespace_reader);
 
-environment pop_scope(environment const & env) {
+environment pop_scope(environment const & env, name const & n) {
     scope_mng_ext ext = get_extension(env);
     if (is_nil(ext.m_namespaces))
         throw exception("invalid end of scope, there are no open namespaces/sections");
+    if (n != head(ext.m_headers))
+        throw exception(sstream() << "invalid end of scope, begin/end mistmatch, scope starts with '" << head(ext.m_headers) << "', and ends with '" << n << "'");
     bool in_section  = head(ext.m_in_section);
     ext.m_namespaces = tail(ext.m_namespaces);
+    ext.m_headers    = tail(ext.m_headers);
     ext.m_in_section = tail(ext.m_in_section);
     environment r = update(env, ext);
     for (auto const & t : get_exts()) {
@@ -146,15 +151,21 @@ static int using_namespace_objects(lua_State * L) {
 static int push_scope(lua_State * L) {
     int nargs = lua_gettop(L);
     if (nargs == 1)
-        return push_environment(L, push_scope(to_environment(L, 1), get_io_state(L)));
+        return push_environment(L, push_scope(to_environment(L, 1), get_io_state(L), true));
     else if (nargs == 2)
-        return push_environment(L, push_scope(to_environment(L, 1), get_io_state(L), to_name_ext(L, 2)));
+        return push_environment(L, push_scope(to_environment(L, 1), get_io_state(L), false, to_name_ext(L, 2)));
+    else if (nargs == 3)
+        return push_environment(L, push_scope(to_environment(L, 1), get_io_state(L), lua_toboolean(L, 3), to_name_ext(L, 2)));
     else
-        return push_environment(L, push_scope(to_environment(L, 1), to_io_state(L, 3), to_name_ext(L, 2)));
+        return push_environment(L, push_scope(to_environment(L, 1), to_io_state(L, 4), lua_toboolean(L, 3), to_name_ext(L, 2)));
 }
 
 static int pop_scope(lua_State * L) {
-    return push_environment(L, pop_scope(to_environment(L, 1)));
+    int nargs = lua_gettop(L);
+    if (nargs == 1)
+        return push_environment(L, pop_scope(to_environment(L, 1)));
+    else
+        return push_environment(L, pop_scope(to_environment(L, 1), to_name_ext(L, 2)));
 }
 
 void open_scoped_ext(lua_State * L) {

src/library/scoped_ext.h

@@ -23,9 +23,9 @@ void register_scoped_ext(name const & n, using_namespace_fn use, push_scope_fn p
 /** \brief Use objects defined in the namespace \c n, if \c c is not the anonymous name, then only object from "class" \c c are considered. */
 environment using_namespace(environment const & env, io_state const & ios, name const & n, name const & c = name());
 /** \brief Create a new scope, all scoped extensions are notified. */
-environment push_scope(environment const & env, io_state const & ios, name const & n = name());
+environment push_scope(environment const & env, io_state const & ios, bool section, name const & n = name());
 /** \brief Delete the most recent scope, all scoped extensions are notified. */
-environment pop_scope(environment const & env);
+environment pop_scope(environment const & env, name const & n = name());
 
 name const & get_namespace(environment const & env);
 list<name> const & get_namespaces(environment const & env);

tests/lean/alias.lean

@@ -3,12 +3,12 @@ import logic
 namespace N1
   variable num : Type.{1}
   variable foo : num → num → num
-end
+end N1
 
 namespace N2
   variable val : Type.{1}
   variable foo : val → val → val
-end
+end N2
 
 using N2
 using N1

tests/lean/run/algebra1.lean

@@ -31,7 +31,7 @@ namespace algebra
   := add_struct_rec (fun f, f) s a b
 
   infixl `+`:65 := add
-end
+end algebra
 
 namespace nat
   inductive nat : Type :=
@@ -50,7 +50,7 @@ namespace nat
   definition to_nat (n : num) : nat
   := #algebra
     num_rec zero (λ n, pos_num_rec (succ zero) (λ n r, r + r) (λ n r, r + r + succ zero) n) n
-end
+end nat
 
 namespace algebra
 namespace semigroup
@@ -74,7 +74,7 @@ namespace semigroup
 
   definition is_semigroup [inline] [instance] (g : semigroup) : semigroup_struct (carrier g)
   := semigroup_rec (fun c s, s) g
-end
+end semigroup
 
 namespace monoid
   check semigroup.mul
@@ -100,8 +100,8 @@ namespace monoid
 
   definition is_monoid [inline] [instance] (m : monoid) : monoid_struct (carrier m)
   := monoid_rec (fun c s, s) m
-end
+end monoid
-end
+end algebra
 
 section
   using algebra algebra.semigroup algebra.monoid

tests/lean/run/alias1.lean

@@ -3,12 +3,12 @@ import logic
 namespace N1
   variable num : Type.{1}
   variable foo : num → num → num
-end
+end N1
 
 namespace N2
   variable val : Type.{1}
   variable foo : val → val → val
-end
+end N2
 
 using N1
 using N2

tests/lean/run/alias2.lean

@@ -3,12 +3,12 @@ import logic
 namespace N1
   variable num : Type.{1}
   variable foo : num → num → num
-end
+end N1
 
 namespace N2
   variable val : Type.{1}
   variable foo : val → val → val
-end
+end N2
 
 using N2
 using N1

tests/lean/run/alias3.lean

@@ -10,7 +10,7 @@ namespace N1
     check foo
   end
   check foo
-end
+end N1
 check N1.foo
 
 namespace N2
@@ -22,5 +22,5 @@ namespace N2
     check list
   end
   check list
-end
+end N2
 check N2.list

tests/lean/run/basic.lean

@@ -60,7 +60,7 @@ section
 end
 check @foo.is_proj2.{1}
 check @foo.is_proj3.{1 2}
-end
+end foo
 
 namespace bla
 section
@@ -73,4 +73,4 @@ section
 end
 check @bla.is_proj2.{1 2}
 check @bla.is_proj3.{1 2 3}
-end
+end bla

tests/lean/run/calc.lean

@@ -6,7 +6,7 @@ namespace foo
   axiom le_trans {a b c : num} : le a b → le b c → le a c
   calc_trans le_trans
   infix `≤`:50 := le
-end
+end foo
 
 namespace foo
   theorem T {a b c d : num} : a ≤ b → b ≤ c → c ≤ d → a ≤ d
@@ -14,4 +14,4 @@ namespace foo
      calc a  ≤ b : H1
          ... ≤ c : H2
          ... ≤ d : H3
-end
+end foo

tests/lean/run/choice_ctx.lean

@@ -6,7 +6,7 @@ set_option pp.coercion true
 namespace foo
 theorem trans {a b c : nat} (H1 : a = b) (H2 : b = c) : a = c :=
 trans H1 H2
-end
+end foo
 
 using foo
 

tests/lean/run/class5.lean

@@ -8,7 +8,7 @@ namespace algebra
   := mul_struct_rec (λ f, f) s a b
 
   infixl `*`:75 := mul
-end
+end algebra
 
 namespace nat
   inductive nat : Type :=
@@ -20,7 +20,7 @@ namespace nat
 
   definition mul_struct [instance] : algebra.mul_struct nat
   := algebra.mk_mul_struct mul
-end
+end nat
 
 section
   using algebra nat

tests/lean/run/coe2.lean

@@ -17,4 +17,4 @@ namespace setoid
   inductive morphism (s1 s2 : setoid) : Type :=
   | mk_morphism : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2
 
-end
+end setoid

tests/lean/run/coe3.lean

@@ -27,4 +27,4 @@ namespace setoid
   | mk_morphism2 : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism2 s1 s2
 
   check mk_morphism2
-end
+end setoid

tests/lean/run/coe4.lean

@@ -31,4 +31,4 @@ namespace setoid
 
   check morphism2
   check mk_morphism2
-end
+end setoid

tests/lean/run/coe5.lean

@@ -37,4 +37,4 @@ namespace setoid
 
   check my_struct
   definition tst2 : Type.{4} := my_struct.{1 2}
-end
+end setoid

tests/lean/run/congr_imp_bug.lean

@@ -44,4 +44,4 @@ theorem congr_and_comp [instance] {T : Type} {R : T → T → Prop} {f1 f2 : T
      (C1 : struc R iff f1) (C2 : struc R iff f2) :
    congr.struc R iff (λx, f1 x ∧ f2 x) := congr.compose21 congr_and C1 C2
 
-end
+end congr

tests/lean/run/e10.lean

@@ -5,7 +5,7 @@ namespace nat
   variable nat : Type.{1}
   variable add : nat → nat → nat
   infixl + := add
-end
+end nat
 
 namespace int
   using nat (nat)
@@ -14,7 +14,7 @@ namespace int
   infixl + := add
   variable of_nat : nat → int
   coercion of_nat
-end
+end int
 
 section
   using nat

tests/lean/run/e11.lean

@@ -4,7 +4,7 @@ namespace nat
   variable nat : Type.{1}
   variable add : nat → nat → nat
   infixl + := add
-end
+end nat
 
 namespace int
   using nat (nat)
@@ -13,7 +13,7 @@ namespace int
   infixl + := add
   variable of_nat : nat → int
   coercion of_nat
-end
+end int
 
 section
   -- Using "only" the notation and declarations from the namespaces nat and int

tests/lean/run/e12.lean

@@ -4,7 +4,7 @@ namespace nat
   variable nat : Type.{1}
   variable add : nat → nat → nat
   infixl + := add
-end
+end nat
 
 namespace int
   using nat (nat)
@@ -13,7 +13,7 @@ namespace int
   infixl + := add
   variable of_nat : nat → int
   coercion of_nat
-end
+end int
 
 variables n m : nat.nat
 variables i j : int.int
@@ -35,7 +35,7 @@ namespace int
   definition add_in (a : int) (b : nat) := a + (of_nat b)
   infixl + := add_ni
   infixl + := add_in
-end
+end int
 
 section
   using [notation] nat

tests/lean/run/e13.lean

@@ -4,7 +4,7 @@ namespace nat
   variable nat : Type.{1}
   variable add : nat → nat → nat
   infixl + := add
-end
+end nat
 
 namespace int
   using nat (nat)
@@ -14,8 +14,8 @@ namespace int
   variable of_nat : nat → int
   namespace coercions
     coercion of_nat
-  end
+  end coercions
-end
+end int
 
 using nat
 using int

tests/lean/run/e6.lean

@@ -5,7 +5,7 @@ namespace nat
   variable nat : Type.{1}
   variable add : nat → nat → nat
   infixl + := add
-end
+end nat
 
 namespace int
   using nat (nat)
@@ -14,7 +14,7 @@ namespace int
   infixl + := add
   variable of_nat : nat → int
   coercion of_nat
-end
+end int
 
 using int
 using nat

tests/lean/run/e7.lean

@@ -5,7 +5,7 @@ namespace nat
   variable nat : Type.{1}
   variable add : nat → nat → nat
   infixl + := add
-end
+end nat
 
 namespace int
   using nat (nat)
@@ -14,7 +14,7 @@ namespace int
   infixl + := add
   variable of_nat : nat → int
   coercion of_nat
-end
+end int
 
 using nat
 using int

tests/lean/run/e8.lean

@@ -4,7 +4,7 @@ namespace nat
   variable nat : Type.{1}
   variable add : nat → nat → nat
   infixl + := add
-end
+end nat
 
 namespace int
   using nat (nat)
@@ -13,7 +13,7 @@ namespace int
   infixl + := add
   variable of_nat : nat → int
   coercion of_nat
-end
+end int
 
 -- Using "only" the notation and declarations from the namespaces nat and int
 using [notation] nat

tests/lean/run/e9.lean

@@ -4,7 +4,7 @@ namespace nat
   variable nat : Type.{1}
   variable add : nat → nat → nat
   infixl + := add
-end
+end nat
 
 namespace int
   using nat (nat)
@@ -12,11 +12,11 @@ namespace int
   variable add : int → int → int
   infixl + := add
   variable of_nat : nat → int
-end
+end int
 
 namespace int_coercions
   coercion int.of_nat
-end
+end int_coercions
 
 -- Using "only" the notation and declarations from the namespaces nat and int
 using nat

tests/lean/run/full.lean

@@ -6,4 +6,4 @@ namespace foo
   check x
   set_option pp.full_names true
   check x
-end
+end foo

tests/lean/run/ind7.lean

@@ -6,6 +6,6 @@ namespace list
   check list.{1}
   check cons.{1}
   check list_rec.{1 1}
-end
+end list
 
 check list.list.{1}

tests/lean/run/induniv.lean

@@ -17,7 +17,7 @@ inductive tree (A : Type) : Type :=
 with forest (A : Type) : Type :=
 | nil  : forest A
 | cons : tree A → forest A → forest A
-end
+end Tree
 
 inductive group_struct (A : Type) : Type :=
 | mk_group_struct : (A → A → A) → A → group_struct A

tests/lean/run/local_using.lean

@@ -5,13 +5,13 @@ namespace foo
   variable a : N
   variable f : N → N → N
   infix + := f
-end
+end foo
 
 namespace bla
   variable b : N
   variable f : N → N → N
   infix + := f
-end
+end bla
 
 variable g : N → N → N
 

tests/lean/run/ns1.lean

@@ -3,8 +3,8 @@ import standard
 namespace foo
 namespace boo
 theorem tst : true := trivial
-end
+end boo
-end
+end foo
 
 using foo
 check boo.tst

tests/lean/run/root.lean

@@ -13,8 +13,8 @@ namespace N1
     check N1.N2.foo
     print raw foo
     print raw _root_.foo
-  end
+  end N2
-end
+end N1
 
 
 

tests/lean/run/set2.lean

@@ -15,4 +15,6 @@ section
 
   theorem mem_empty (x : T) : ¬ (x ∈ ∅)
   := not_intro (λH : x ∈ ∅, absurd H ff_ne_tt)
-end
+end
+
+end set

tests/lean/run/t4.lean

@@ -1,7 +1,7 @@
 namespace foo
   definition f.{l} (A : Type.{l}) : Type.{l} := A
   check f.{1}
-end
+end foo
 
 variable N : Type.{1}
 section

tests/lean/run/t5.lean

@@ -4,8 +4,8 @@ namespace foo
   namespace tst
     variable N : Type.{3}
     print raw N
-  end
+  end tst
-end
+end foo
 print raw N
 namespace foo
   print raw N
@@ -15,5 +15,5 @@ namespace foo
       variable N : Type.{4} -- Shadow previous ones.
       print raw N
     end
-  end
+  end tst
-end
+end  foo

tests/lean/run/univ1.lean

@@ -6,7 +6,7 @@ definition F (X : Type) : Type := (X → Prop) → Prop
 hypothesis unfold.{l} : I.{l} → F I.{l}
 hypothesis fold.{l}   : F I.{l} → I.{l}
 hypothesis iso1 : ∀x, fold (unfold x) = x
-end
+end S1
 
 namespace S2
 universe u
@@ -15,7 +15,7 @@ definition F (X : Type) : Type := (X → Prop) → Prop
 hypothesis unfold : I → F I
 hypothesis fold   : F I → I
 hypothesis iso1 : ∀x, fold (unfold x) = x
-end
+end S2
 
 
 namespace S3
@@ -26,4 +26,4 @@ section
   hypothesis fold   : F I → I
   hypothesis iso1 : ∀x, fold (unfold x) = x
 end
-end
+end S3

tests/lean/run/univ_bug1.lean

@@ -24,3 +24,5 @@ simplifies_to_rec (λx, x) C
 theorem simp_app [instance] (S T : Type) (f1 f2 : S → T) (s1 s2 : S)
    (C1 : simplifies_to f1 f2) (C2 : simplifies_to s1 s2) : simplifies_to (f1 s1) (f2 s2) :=
 mk (congr (get_eq C1) (get_eq C2))
+
+end simp

tests/lean/slow/list_elab2.lean

@@ -188,46 +188,6 @@ list_induction_on l
       append x (y :: l') = (y :: l') ++ [ x ] : append_eq_concat _ _
         ... = concat (reverse (reverse (y :: l'))) [ x ] : {symm (reverse_reverse _)}
 	... = reverse (x :: (reverse (y :: l'))) : refl _)
+end
+end list
 
-exit
--- Head and tail
--- -------------
-
-definition head (x0 : T) : list T → T := list_rec x0 (fun x l h, x)
-
-theorem head_nil (x0 : T) : head x0 (@nil T) = x0 := refl _
-
-theorem head_cons (x : T) (x0 : T) (t : list T) : head x0 (x :: t) = x := refl _
-
-theorem head_concat (s t : list T) (x0 : T) : s ≠ nil → (head x0 (s ++ t) = head x0 s) :=
-list_cases_on s
-  (take H : nil ≠ nil, absurd_elim (head x0 (concat nil t) = head x0 nil) (refl nil) H)
-  (take x s,
-    take H : cons x s ≠ nil,
-    calc
-      head x0 (concat (cons x s) t) = head x0 (cons x (concat s t)) : {cons_concat _ _ _}
-        ... = x : {head_cons _ _ _}
-        ... = head x0 (cons x s) : {symm ( head_cons x x0 s)})
-
-definition tail : list T → list T := list_rec nil (fun x l b, l)
-
-theorem tail_nil : tail (@nil T) = nil := refl _
-
-theorem tail_cons (x : T) (l : list T) : tail (cons x l) = l := refl _
-
-theorem cons_head_tail (x0 : T) (l : list T) : l ≠ nil → (head x0 l) :: (tail l) = l :=
-list_cases_on l
-  (assume H : nil ≠ nil, absurd_elim _ (refl _) H)
-  (take x l, assume H : cons x l ≠ nil, refl _)
-
-
--- List membership
--- ---------------
-
-definition mem (x : T) : list T → Prop := list_rec false (fun y l H, x = y ∨ H)
-
-infix `∈` : 50 := mem
-
-theorem mem_nil (x : T) : mem x nil ↔ false := iff_refl _
-
-theorem mem_cons (x : T) (y : T) (l : list T) : mem x (cons y l) ↔ (x = y ∨ mem x l) := iff_refl _

tests/lean/slow/nat_wo_hints.lean

@@ -23,7 +23,7 @@ definition to_nat [coercion] [inline] (n : num) : ℕ
 namespace helper_tactics
   definition apply_refl := apply @refl
   tactic_hint apply_refl
-end
+end helper_tactics
 using helper_tactics
 
 theorem nat_rec_zero {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) : nat_rec x f 0 = x
@@ -1418,4 +1418,7 @@ theorem dist_eq_intro {n m k l : ℕ} (H : n + m = k + l) : dist n k = dist l m
     dist n k = dist (n + m) (k + m) : symm (dist_add_right n m k)
       ... = dist (k + l) (k + m) : {H}
       ... = dist l m : dist_add_left k l m
-end --namespace nat
+
+
+
+end nat

tests/lean/t14.lean

@@ -4,7 +4,7 @@ namespace foo
   variable a : A
   variable x : A
   variable c : A
-end
+end foo
 
 section
   using foo (renaming a->b x->y) (hiding c)
@@ -34,7 +34,7 @@ end
 namespace foo
   variable f : A → A → A
   infix `*`:75 := f
-end
+end foo
 
 section
   using foo

tests/lean/t3.lean

@@ -4,7 +4,7 @@ namespace tst
   universe v
   print raw Type.{v}
   print raw Type.{tst.v}
-end
+end tst
 print raw Type.{tst.v}
 print raw Type.{v}  -- Error: alias 'v' is not available anymore
 section
@@ -20,8 +20,8 @@ namespace tst
   print raw Type.{u}
   namespace foo
     universe U
-  end
+  end foo
-end
+end tst
 print raw Type.{tst.foo.U}
 namespace tst.foo    -- Error: we cannot use qualified names in declarations
 universe full.name.U -- Error: we cannot use qualified names in declarations
@@ -29,9 +29,9 @@ namespace tst
   namespace foo
     print raw Type.{v}  -- Remark: alias 'v' for 'tst.v' is available again
     print raw Type.{U}  -- Remark: alias 'U' for 'tst.foo.U' is available again
-  end
+  end foo
-end
+end tst
 namespace bla
   universe u -- Error: we cannot shadow universe levels
-end
+end bla
 print raw Type.{bla.u} -- Error: we failed to declare bla.u

tests/lean/t4.lean

@@ -34,17 +34,17 @@ namespace tst
   variable M : Type.{2}
   print raw N -- Two possible interpretations N and tst.N
   print raw tst.N -- Only one interpretation
-end
+end tst
 print raw N -- Only one interpretation
 namespace foo
   variable M : Type.{3}
   print raw M -- Only one interpretation
-end
+end foo
 check tst.M
 check foo.M
 namespace foo
   check M
-end
+end foo
 check M -- Error
 
 print "ok"

tests/lean/t5.lean

@@ -8,6 +8,6 @@ namespace foo
   check h
   definition q [private] : N := f a
   check q
-end
+end foo
 check foo.h
 check q -- Error q is now hidden

tests/lean/t9.lean

@@ -11,10 +11,10 @@ namespace foo
   infixl + := add
   infixl * := mul
   check a+b*a
-end
+end foo
 -- Notation is not avaiable outside the namespace
 check a+b*a
 namespace foo
   -- Notation is restored
   check a+b*a
-end
+end foo

tests/lua/scope.lua

@@ -42,7 +42,7 @@ function get_num_coercions(env)
 end
 for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end)
 assert(get_num_coercions(env) == 3)
-env = pop_scope(env)
+env = pop_scope(env, "tst")
 print("---------")
 for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end)
 assert(get_num_coercions(env) == 1)
@@ -67,7 +67,7 @@ assert(get_num_coercions(env) == 6)
 print("---------")
 env = pop_scope(env)
 assert(get_num_coercions(env) == 3)
-env = pop_scope(env)
+env = pop_scope(env, "tst")
 for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end)
 assert(get_num_coercions(env) == 1)
 env = push_scope(env, "tst")