feat(frontends/lean): flip definition modifiers position, now they must occur after the identifier

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

src/frontends/lean/decl_cmds.cpp

@@ -178,12 +178,12 @@ levels collect_section_levels(level_param_names const & ls, parser & p) {
 }
 
 environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque) {
+    name n = p.check_id_next("invalid declaration, identifier expected");
+    check_atomic(n);
     bool is_private = false;
     parse_modifiers(p, is_private, is_opaque);
     if (is_theorem && !is_opaque)
         throw exception("invalid theorem declaration, theorems cannot be transparent");
-    name n = p.check_id_next("invalid declaration, identifier expected");
-    check_atomic(n);
     environment env = p.env();
     name real_n; // real name for this declaration
     if (is_private) {

tests/lean/bug1.lean

@@ -1,5 +1,5 @@
-definition [inline] bool : Type.{1}           := Type.{0}
-definition [inline] and  (p q : bool) : bool  := ∀ c : bool, (p → q → c) → c
+definition bool [inline] : Type.{1}           := Type.{0}
+definition and  [inline] (p q : bool) : bool  := ∀ c : bool, (p → q → c) → c
 infixl `∧` 25 := and
 
 variable a : bool
@@ -21,4 +21,3 @@ theorem and_intro (p q : bool) (H1 : p) (H2 : q) : p ∧ q
 := fun (c : bool) (H : p -> q -> c), H H1 H2
 
 check and_intro
-

tests/lean/calc1.lean

@@ -1,5 +1,5 @@
 variable A : Type.{1}
-definition [inline] bool : Type.{1} := Type.{0}
+definition bool [inline] : Type.{1} := Type.{0}
 variable eq : A → A → bool
 infixl `=` 50 := eq
 axiom subst (P : A → bool) (a b : A) (H1 : a = b) (H2 : P a) : P b

tests/lean/run/ind5.lean

@@ -1,4 +1,4 @@
-definition [inline] Bool : Type.{1} := Type.{0}
+definition Bool [inline] : Type.{1} := Type.{0}
 
 inductive or (A B : Bool) : Bool :=
 | or_intro_left  : A → or A B

tests/lean/run/n3.lean

@@ -1,4 +1,4 @@
-definition [inline] Bool : Type.{1} := Type.{0}
+definition Bool [inline] : Type.{1} := Type.{0}
 variable N : Type.{1}
 variable and : Bool → Bool → Bool
 infixr `∧` 35 := and

tests/lean/run/n4.lean

@@ -1,4 +1,4 @@
-definition [inline] Bool : Type.{1} := Type.{0}
+definition Bool [inline] : Type.{1} := Type.{0}
 section
   variable N : Type.{1}
   variables a b c : N

tests/lean/run/t9.lean

@@ -1,4 +1,4 @@
-definition [inline] bool : Type.{1} := Type.{0}
+definition bool [inline] : Type.{1} := Type.{0}
 definition and (p q : bool) : bool
 := ∀ c : bool, (p → q → c) →  c
 infixl `∧` 25 := and
@@ -12,4 +12,3 @@ theorem and_comm (p q : bool) (H : p ∧ q) : q ∧ p
 := have H1 : p, from and_elim_left p q H,
    have H2 : q, from and_elim_right p q H,
    show q ∧ p, from and_intro q p H2 H1
-

tests/lean/t4.lean

@@ -1,4 +1,4 @@
-definition [inline] Bool : Type.{1} := Type.{0}
+definition Bool [inline] : Type.{1} := Type.{0}
 variable N : Type.{1}
 check N
 variable a : N

tests/lean/t5.lean

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

tests/lean/t7.lean

@@ -5,7 +5,7 @@ section
   parameter   R : A → A → Bool
   parameter   B : Type
   definition  id (a : A) : A := a
-  definition [private] refl : Bool := ∀ (a : A), R a a
+  definition  refl [private] : Bool := ∀ (a : A), R a a
   definition  symm : Bool := ∀ (a b : A), R a b → R b a
   definition  trans : Bool := ∀ (a b c : A), R a b → R b c → R a c
   definition  equivalence : Bool := and (and refl symm) trans

tests/lean/t7.lean.expected.out

@@ -2,4 +2,4 @@ id.{2} : Pi {A : Type.{2}} (a : A), A
 trans.{1} : Pi {A : Type} (R : A -> A -> Bool), Bool
 symm.{1} : Pi {A : Type} (R : A -> A -> Bool), Bool
 equivalence.{1} : Pi {A : Type} (R : A -> A -> Bool), Bool
-fun {A : Type.{l_1}} (R : A -> A -> Bool), (and (and (private.2595647076.refl.{l_1} A R) (symm.{l_1} A R)) (trans.{l_1} A R))
+fun {A : Type.{l_1}} (R : A -> A -> Bool), (and (and (private.3808308840.refl.{l_1} A R) (symm.{l_1} A R)) (trans.{l_1} A R))