feat(frontends/lean): allow persistent notation declaration in sections (when they do not contain parameters)

see issue #554

src/frontends/lean/notation_cmd.cpp

@@ -625,8 +625,6 @@ struct notation_modifiers {
 };
 
 static environment notation_cmd_core(parser & p, bool overload, bool reserve, bool persistent) {
-    if (persistent)
-        check_not_in_parametric_section(p);
     notation_modifiers mods;
     mods.parse(p);
     flet<bool> set_allow_local(g_allow_local, in_context(p.env()) || !persistent);
@@ -640,8 +638,6 @@ static environment notation_cmd_core(parser & p, bool overload, bool reserve, bo
 }
 
 static environment mixfix_cmd(parser & p, mixfix_kind k, bool overload, bool reserve, bool persistent) {
-    if (persistent)
-        check_not_in_parametric_section(p);
     notation_modifiers mods;
     mods.parse(p);
     flet<bool> set_allow_local(g_allow_local, in_context(p.env()) || !persistent);

src/frontends/lean/util.cpp

@@ -70,19 +70,6 @@ void check_in_context_or_section(parser const & p) {
         throw exception(sstream() << "invalid command, it must be used in a (local) context or section");
 }
 
-bool in_parametric_section(parser const & p) {
-    return in_section(p.env()) && p.has_params();
-}
-
-void check_not_in_parametric_section(parser const & p) {
-    if (in_parametric_section(p))
-        throw exception(sstream() << "invalid command, it cannot be used in sections containing parameters");
-}
-
-bool in_context_or_parametric_section(parser const & p) {
-    return in_context(p.env()) || in_parametric_section(p);
-}
-
 bool is_root_namespace(name const & n) {
     return n == get_root_tk();
 }

src/frontends/lean/util.h

@@ -29,9 +29,6 @@ void check_command_period_open_binder_or_eof(parser const & p);
 void check_atomic(name const & n);
 void check_in_context(parser const & p);
 void check_in_context_or_section(parser const & p);
-void check_not_in_parametric_section(parser const & p);
-bool in_parametric_section(parser const & p);
-bool in_context_or_parametric_section(parser const & p);
 bool is_root_namespace(name const & n);
 name remove_root_prefix(name const & n);
 /** \brief Return the local levels in \c ls that are not tagged as variables.

tests/lean/run/sec_notation.lean

@@ -0,0 +1,15 @@
+open nat
+
+section
+  parameter (A : Type)
+  definition f (a b : A) : A := a
+
+  definition add2 (a : nat) : nat := a + 2
+
+  postfix `+.2`:100 := add2
+
+  eval 3 +.2
+end
+
+example : 3 +.2 = 5 :=
+rfl