From e24225fabf488998f24c06409add0e8ffbc76772 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 21 Oct 2014 15:27:45 -0700
Subject: [PATCH] feat(frontends/lean): validate infixl/infixr/postfix/prefix
 declarations against reserved notations

---
 library/algebra/binary.lean           |   6 +-
 library/data/sum.lean                 |   3 +-
 library/data/vector.lean              |   2 +-
 src/frontends/lean/notation_cmd.cpp   | 104 ++++++++++++++++++++------
 tests/lean/run/algebra1.lean          |   6 +-
 tests/lean/run/calc.lean              |   2 +-
 tests/lean/run/class4.lean            |   2 +-
 tests/lean/run/class5.lean            |   2 +-
 tests/lean/run/class_coe.lean         |   4 +-
 tests/lean/run/coe2.lean              |   2 +-
 tests/lean/run/coe3.lean              |   2 +-
 tests/lean/run/coe4.lean              |   2 +-
 tests/lean/run/coe5.lean              |   2 +-
 tests/lean/run/coe8.lean              |   4 +-
 tests/lean/run/group.lean             |   4 +-
 tests/lean/run/group2.lean            |   4 +-
 tests/lean/run/nat_bug2.lean          |   4 +-
 tests/lean/run/nat_bug3.lean          |   4 +-
 tests/lean/run/nat_bug4.lean          |   4 +-
 tests/lean/run/nat_bug5.lean          |   4 +-
 tests/lean/run/nat_bug6.lean          |   4 +-
 tests/lean/run/nat_bug7.lean          |   2 +-
 tests/lean/run/nat_coe.lean           |   4 +-
 tests/lean/run/not_bug1.lean          |   2 +-
 tests/lean/run/occurs_check_bug1.lean |   2 +-
 tests/lean/run/over_subst.lean        |  10 +--
 tests/lean/run/ppbeta.lean            |   2 +-
 tests/lean/run/set.lean               |   2 +-
 tests/lean/run/set2.lean              |   2 +-
 tests/lean/run/sum_bug.lean           |   4 +-
 tests/lean/run/tactic23.lean          |   2 +-
 tests/lean/slow/list_elab2.lean       |   4 +-
 tests/lean/slow/nat_bug2.lean         |  18 ++---
 tests/lean/slow/nat_wo_hints.lean     |  18 ++---
 tests/lean/slow/path_groupoids.lean   |   2 +-
 35 files changed, 153 insertions(+), 92 deletions(-)

diff --git a/library/algebra/binary.lean b/library/algebra/binary.lean
index d544d40f5..452fb6331 100644
--- a/library/algebra/binary.lean
+++ b/library/algebra/binary.lean
@@ -8,7 +8,7 @@ namespace binary
   context
     variable {A : Type}
     variable f : A → A → A
-    infixl `*`:75 := f
+    infixl `*` := f
     definition commutative := ∀{a b}, a*b = b*a
     definition associative := ∀{a b c}, (a*b)*c = a*(b*c)
   end
@@ -18,7 +18,7 @@ namespace binary
     variable {f : A → A → A}
     variable H_comm : commutative f
     variable H_assoc : associative f
-    infixl `*`:75 := f
+    infixl `*` := f
     theorem left_comm : ∀a b c, a*(b*c) = b*(a*c) :=
     take a b c, calc
       a*(b*c) = (a*b)*c  : H_assoc⁻¹
@@ -36,7 +36,7 @@ namespace binary
     variable {A : Type}
     variable {f : A → A → A}
     variable H_assoc : associative f
-    infixl `*`:75 := f
+    infixl `*` := f
     theorem assoc4helper (a b c d) : (a*b)*(c*d) = a*((b*c)*d) :=
     calc
       (a*b)*(c*d) = a*(b*(c*d)) : H_assoc
diff --git a/library/data/sum.lean b/library/data/sum.lean
index 12d9a79a9..c3a1311a0 100644
--- a/library/data/sum.lean
+++ b/library/data/sum.lean
@@ -14,7 +14,8 @@ inductive sum (A B : Type) : Type :=
 namespace sum
   notation A ⊎ B := sum A B
   namespace extra_notation
-    infixr `+`:25 := sum    -- conflicts with notation for addition
+    reserve infixr `+`:25 -- conflicts with notation for addition
+    infixr `+` := sum
   end extra_notation
 
   variables {A B : Type}
diff --git a/library/data/vector.lean b/library/data/vector.lean
index d8566e1e5..2cd251ee5 100644
--- a/library/data/vector.lean
+++ b/library/data/vector.lean
@@ -84,7 +84,7 @@ namespace vector
   definition concat {n m : ℕ} (v : vector T n) (w : vector T m) : vector T (n + m) :=
   vector.rec (cast_subst (!add.zero_left⁻¹) w) (λx n w' u, cast_subst (!add.succ_left⁻¹) (x::u)) v
 
-  infixl `++`:65 := concat
+  notation h ++ t := concat h t
 
   theorem nil_concat {n : ℕ} (v : vector T n) : nil ++ v = cast_subst (!add.zero_left⁻¹) v := rfl
 
diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp
index 082fa143c..f78a42d80 100644
--- a/src/frontends/lean/notation_cmd.cpp
+++ b/src/frontends/lean/notation_cmd.cpp
@@ -67,53 +67,113 @@ using notation::mk_ext_lua_action;
 using notation::transition;
 using notation::action;
 
-static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool reserve )
+static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool reserve)
 -> pair<notation_entry, optional<token_entry>> {
     std::string tk = parse_symbol(p, "invalid notation declaration, quoted symbol or identifier expected");
+    char const * tks = tk.c_str();
+    environment const & env = p.env();
+    optional<token_entry> new_token;
     optional<unsigned> prec;
+
+    optional<parse_table> reserved_pt;
+    optional<action> reserved_action;
+    if (!reserve) {
+        if (k == mixfix_kind::prefix) {
+            if (auto at = get_reserved_nud_table(p.env()).find(tks)) {
+                reserved_pt     = at->second;
+                reserved_action = at->first;
+            }
+        } else {
+            if (auto at = get_reserved_led_table(p.env()).find(tks)) {
+                reserved_pt     = at->second;
+                reserved_action = at->first;
+            }
+        }
+    }
+
     if (p.curr_is_token(get_colon_tk())) {
+        if (reserved_pt)
+            throw parser_error("invalid notation declaration, invalid ':' occurrence "
+                               "(declaration matches reserved notation)", p.pos());
         p.next();
         prec = parse_precedence(p, "invalid notation declaration, numeral or 'max' expected");
     }
-    environment const & env = p.env();
-    optional<token_entry> new_token;
+
     if (!prec) {
         prec = get_precedence(get_token_table(env), tk.c_str());
     } else if (prec != get_precedence(get_token_table(env), tk.c_str())) {
         new_token = token_entry(tk.c_str(), *prec);
     }
 
-    if (!prec)
+    if (!prec) {
+        lean_assert(!reserved_pt);
         throw parser_error("invalid notation declaration, precedence was not provided, "
                            "and it is not set for the given symbol, "
                            "solution: use the 'precedence' command", p.pos());
+    }
+
     if (k == mixfix_kind::infixr && *prec == 0)
         throw parser_error("invalid infixr declaration, precedence must be greater than zero", p.pos());
-    expr f;
+
+    if (reserved_action) {
+        switch (k) {
+        case mixfix_kind::infixl:
+            if (reserved_action->kind() != notation::action_kind::Expr || reserved_action->rbp() != *prec)
+                throw parser_error("invalid infixl declaration, declaration conflicts with reserved notation", p.pos());
+            break;
+        case mixfix_kind::infixr:
+            if (reserved_action->kind() != notation::action_kind::Expr || reserved_action->rbp() != *prec-1)
+                throw parser_error("invalid infixr declaration, declaration conflicts with reserved notation", p.pos());
+            break;
+        case mixfix_kind::postfix:
+            if (reserved_action->kind() != notation::action_kind::Skip)
+                throw parser_error("invalid postfix declaration, declaration conflicts with reserved notation", p.pos());
+            break;
+        case mixfix_kind::prefix:
+            if (reserved_action->kind() != notation::action_kind::Expr || reserved_action->rbp() != *prec)
+                throw parser_error("invalid prefix declaration, declaration conflicts with reserved notation", p.pos());
+            break;
+        }
+    }
+
     if (reserve) {
         // reserve notation commands do not have a denotation
+        expr dummy = mk_Prop();
         if (p.curr_is_token(get_assign_tk()))
             throw parser_error("invalid reserve notation, found `:=`", p.pos());
+        switch (k) {
+        case mixfix_kind::infixl:
+            return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec))),
+                                          dummy, overload, reserve), new_token);
+        case mixfix_kind::infixr:
+            return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec-1))),
+                                          dummy, overload, reserve), new_token);
+        case mixfix_kind::postfix:
+            return mk_pair(notation_entry(false, to_list(transition(tks, mk_skip_action())),
+                                          dummy, overload, reserve), new_token);
+        case mixfix_kind::prefix:
+            return mk_pair(notation_entry(true, to_list(transition(tks, mk_expr_action(*prec))),
+                                          dummy, overload, reserve), new_token);
+        }
     } else {
         p.check_token_next(get_assign_tk(), "invalid notation declaration, ':=' expected");
         auto f_pos = p.pos();
-        f     = p.parse_expr();
+        expr f     = p.parse_expr();
         check_notation_expr(f, f_pos);
-    }
-    char const * tks = tk.c_str();
-    switch (k) {
-    case mixfix_kind::infixl:
-        return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec))),
-                                      mk_app(f, Var(1), Var(0)), overload, reserve), new_token);
-    case mixfix_kind::infixr:
-        return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec-1))),
-                                      mk_app(f, Var(1), Var(0)), overload, reserve), new_token);
-    case mixfix_kind::postfix:
-        return mk_pair(notation_entry(false, to_list(transition(tks, mk_skip_action())),
-                                      mk_app(f, Var(0)), overload, reserve), new_token);
-    case mixfix_kind::prefix:
-        return mk_pair(notation_entry(true, to_list(transition(tks, mk_expr_action(*prec))),
-                                      mk_app(f, Var(0)), overload, reserve), new_token);
+        switch (k) {
+        case mixfix_kind::infixl:
+            return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec))),
+                                          mk_app(f, Var(1), Var(0)), overload, reserve), new_token);
+        case mixfix_kind::infixr:
+            return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec-1))),
+                                          mk_app(f, Var(1), Var(0)), overload, reserve), new_token);
+        case mixfix_kind::postfix:
+            return mk_pair(notation_entry(false, to_list(transition(tks, mk_skip_action())),
+                                          mk_app(f, Var(0)), overload, reserve), new_token);
+        case mixfix_kind::prefix:
+            return mk_pair(notation_entry(true, to_list(transition(tks, mk_expr_action(*prec))),
+                                          mk_app(f, Var(0)), overload, reserve), new_token);
+        }
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }
@@ -357,7 +417,7 @@ static notation_entry parse_notation_core(parser & p, bool overload, bool reserv
                 break;
             }}
             if (p.curr_is_token(get_colon_tk()))
-                throw parser_error("invalid notation declaration, invalid `:` occurrence "
+                throw parser_error("invalid notation declaration, invalid ':' occurrence "
                                    "(declaration prefix matches reserved notation)", p.pos());
         } else {
             reserved_pt = optional<parse_table>();
diff --git a/tests/lean/run/algebra1.lean b/tests/lean/run/algebra1.lean
index ed22f6ce3..dec2c3244 100644
--- a/tests/lean/run/algebra1.lean
+++ b/tests/lean/run/algebra1.lean
@@ -7,7 +7,7 @@ context
   variable f   : A → A → A
   variable one : A
   variable inv : A → A
-  infixl `*`:75     := f
+  infixl `*`     := f
   postfix `^-1`:100 := inv
   definition is_assoc := ∀ a b c, (a*b)*c = a*b*c
   definition is_id    := ∀ a, a*one = a
@@ -24,12 +24,12 @@ namespace algebra
   definition mul  {A : Type} [s : mul_struct A] (a b : A)
   := mul_struct.rec (fun f, f) s a b
 
-  infixl `*`:75 := mul
+  infixl `*` := mul
 
   definition add  {A : Type} [s : add_struct A] (a b : A)
   := add_struct.rec (fun f, f) s a b
 
-  infixl `+`:65 := add
+  infixl `+` := add
 end algebra
 
 open algebra
diff --git a/tests/lean/run/calc.lean b/tests/lean/run/calc.lean
index dbc6f286e..0a312687d 100644
--- a/tests/lean/run/calc.lean
+++ b/tests/lean/run/calc.lean
@@ -5,7 +5,7 @@ namespace foo
   constant le : num → num → Prop
   axiom le_trans {a b c : num} : le a b → le b c → le a c
   calc_trans le_trans
-  infix `≤`:50 := le
+  infix `≤` := le
 end foo
 
 namespace foo
diff --git a/tests/lean/run/class4.lean b/tests/lean/run/class4.lean
index 4d1f3f544..0d03db227 100644
--- a/tests/lean/run/class4.lean
+++ b/tests/lean/run/class4.lean
@@ -10,7 +10,7 @@ namespace nat
 definition add (x y : nat)
 := nat.rec x (λ n r, succ r) y
 
-infixl `+`:65 := add
+infixl `+` := add
 
 theorem add_zero_left (x : nat) : x + zero = x
 := refl _
diff --git a/tests/lean/run/class5.lean b/tests/lean/run/class5.lean
index bbb197123..f38cea46a 100644
--- a/tests/lean/run/class5.lean
+++ b/tests/lean/run/class5.lean
@@ -7,7 +7,7 @@ namespace algebra
   definition mul {A : Type} [s : mul_struct A] (a b : A)
   := mul_struct.rec (λ f, f) s a b
 
-  infixl `*`:75 := mul
+  infixl `*` := mul
 end algebra
 
 open algebra
diff --git a/tests/lean/run/class_coe.lean b/tests/lean/run/class_coe.lean
index b6d84c8d4..52151aa59 100644
--- a/tests/lean/run/class_coe.lean
+++ b/tests/lean/run/class_coe.lean
@@ -12,7 +12,7 @@ mk : (A → A → A) → add_struct A
 definition add {A : Type} {S : add_struct A} (a b : A) : A :=
 add_struct.rec (λ m, m) S a b
 
-infixl `+`:65 := add
+infixl `+` := add
 
 definition add_nat_struct  [instance] : add_struct nat := add_struct.mk nat_add
 definition add_int_struct  [instance] : add_struct int := add_struct.mk int_add
@@ -48,7 +48,7 @@ check 0 + x
 check x + 0
 namespace foo
 constant eq {A : Type} : A → A → Prop
-infixl `=`:50 := eq
+infixl `=` := eq
 definition id (A : Type) (a : A) := a
 notation A `=` B `:` C := @eq C A B
 check nat_to_int n + nat_to_int m = (n + m) : int
diff --git a/tests/lean/run/coe2.lean b/tests/lean/run/coe2.lean
index 8713dc243..5e51984c1 100644
--- a/tests/lean/run/coe2.lean
+++ b/tests/lean/run/coe2.lean
@@ -10,7 +10,7 @@ namespace setoid
   definition eqv {s : setoid} : carrier s → carrier s → Prop
   := setoid.rec (λ a eqv, eqv) s
 
-  infix `≈`:50 := eqv
+  infix `≈` := eqv
 
   coercion carrier
 
diff --git a/tests/lean/run/coe3.lean b/tests/lean/run/coe3.lean
index 1931874af..0bb593bec 100644
--- a/tests/lean/run/coe3.lean
+++ b/tests/lean/run/coe3.lean
@@ -10,7 +10,7 @@ namespace setoid
   definition eqv {s : setoid} : carrier s → carrier s → Prop
   := setoid.rec (λ a eqv, eqv) s
 
-  infix `≈`:50 := eqv
+  infix `≈` := eqv
 
   coercion carrier
 
diff --git a/tests/lean/run/coe4.lean b/tests/lean/run/coe4.lean
index 0406d9a09..08c4e4097 100644
--- a/tests/lean/run/coe4.lean
+++ b/tests/lean/run/coe4.lean
@@ -15,7 +15,7 @@ namespace setoid
   definition eqv {s : setoid} : carrier s → carrier s → Prop
   := setoid.rec (λ a eqv, eqv) s
 
-  infix `≈`:50 := eqv
+  infix `≈` := eqv
 
   coercion carrier
 
diff --git a/tests/lean/run/coe5.lean b/tests/lean/run/coe5.lean
index 8752fe847..41420afe8 100644
--- a/tests/lean/run/coe5.lean
+++ b/tests/lean/run/coe5.lean
@@ -15,7 +15,7 @@ namespace setoid
   definition eqv {s : setoid} : carrier s → carrier s → Prop
   := setoid.rec (λ a eqv, eqv) s
 
-  infix `≈`:50 := eqv
+  infix `≈` := eqv
 
   coercion carrier
 
diff --git a/tests/lean/run/coe8.lean b/tests/lean/run/coe8.lean
index bb8e3f218..510491854 100644
--- a/tests/lean/run/coe8.lean
+++ b/tests/lean/run/coe8.lean
@@ -6,8 +6,8 @@ constant of_nat : nat → int
 coercion of_nat
 constant nat_add : nat → nat → nat
 constant int_add : int → int → int
-infixl `+`:65 := int_add
-infixl `+`:65 := nat_add
+infixl `+` := int_add
+infixl `+` := nat_add
 
 print "================"
 constant tst (n m : nat) : @eq int (of_nat n + of_nat m) (n + m)
diff --git a/tests/lean/run/group.lean b/tests/lean/run/group.lean
index ef3cb750e..3c4dc3b9f 100644
--- a/tests/lean/run/group.lean
+++ b/tests/lean/run/group.lean
@@ -5,7 +5,7 @@ context
   variable f   : A → A → A
   variable one : A
   variable inv : A → A
-  infixl `*`:75     := f
+  infixl `*`   := f
   postfix `^-1`:100 := inv
   definition is_assoc := ∀ a b c, (a*b)*c = a*b*c
   definition is_id    := ∀ a, a*one = a
@@ -29,7 +29,7 @@ check group_struct
 definition mul {A : Type} {s : group_struct A} (a b : A) : A
 := group_struct.rec (λ mul one inv h1 h2 h3, mul) s a b
 
-infixl `*`:75 := mul
+infixl `*` := mul
 
 constant  G1 : group.{1}
 constant  G2 : group.{1}
diff --git a/tests/lean/run/group2.lean b/tests/lean/run/group2.lean
index 5c45ff341..50f3c82c8 100644
--- a/tests/lean/run/group2.lean
+++ b/tests/lean/run/group2.lean
@@ -5,7 +5,7 @@ context
   variable f   : A → A → A
   variable one : A
   variable inv : A → A
-  infixl `*`:75     := f
+  infixl `*`     := f
   postfix `^-1`:100 := inv
   definition is_assoc := ∀ a b c, (a*b)*c = a*b*c
   definition is_id    := ∀ a, a*one = a
@@ -31,7 +31,7 @@ check group_struct
 definition mul {A : Type} [s : group_struct A] (a b : A) : A
 := group_struct.rec (λ mul one inv h1 h2 h3, mul) s a b
 
-infixl `*`:75 := mul
+infixl `*` := mul
 
 section
   variable  G1 : group
diff --git a/tests/lean/run/nat_bug2.lean b/tests/lean/run/nat_bug2.lean
index 3dbce8b55..864ecf419 100644
--- a/tests/lean/run/nat_bug2.lean
+++ b/tests/lean/run/nat_bug2.lean
@@ -14,8 +14,8 @@ definition add (x y : nat) : nat
 := plus x y
 constant le : nat → nat → Prop
 
-infixl `+`:65 := add
-infix `≤`:50  := le
+infixl `+` := add
+infix `≤`  := le
 axiom add_one (n:nat) : n + (succ zero) = succ n
 axiom add_le_right {n m : nat} (H : n ≤ m) (k : nat) : n + k ≤ m + k
 
diff --git a/tests/lean/run/nat_bug3.lean b/tests/lean/run/nat_bug3.lean
index 53e5c5c8f..98a05aeef 100644
--- a/tests/lean/run/nat_bug3.lean
+++ b/tests/lean/run/nat_bug3.lean
@@ -14,8 +14,8 @@ definition add (x y : nat) : nat
 := plus x y
 constant le : nat → nat → Prop
 
-infixl `+`:65 := add
-infix `≤`:50  := le
+infixl `+` := add
+infix `≤`  := le
 axiom add_one (n:nat) : n + (succ zero) = succ n
 axiom add_le_right_inv {n m k : nat} (H : n + k ≤ m + k) : n ≤ m
 
diff --git a/tests/lean/run/nat_bug4.lean b/tests/lean/run/nat_bug4.lean
index 03f7764d5..a197e11f7 100644
--- a/tests/lean/run/nat_bug4.lean
+++ b/tests/lean/run/nat_bug4.lean
@@ -6,9 +6,9 @@ zero : nat,
 succ : nat → nat
 namespace nat
 definition add (x y : nat) : nat := nat.rec x (λn r, succ r) y
-infixl `+`:65 := add
+infixl `+` := add
 definition mul (n m : nat) := nat.rec zero (fun m x, x + n) m
-infixl `*`:75 := mul
+infixl `*` := mul
 
 axiom mul_succ_right (n m : nat) : n * succ m = n * m + n
 open eq
diff --git a/tests/lean/run/nat_bug5.lean b/tests/lean/run/nat_bug5.lean
index b4859dd99..42dee77e5 100644
--- a/tests/lean/run/nat_bug5.lean
+++ b/tests/lean/run/nat_bug5.lean
@@ -7,9 +7,9 @@ succ : nat → nat
 
 namespace nat
 definition add (x y : nat) : nat := nat.rec x (λn r, succ r) y
-infixl `+`:65 := add
+infixl `+` := add
 definition mul (n m : nat) := nat.rec zero (fun m x, x + n) m
-infixl `*`:75 := mul
+infixl `*` := mul
 
 axiom add_one (n:nat) : n + (succ zero) = succ n
 axiom mul_zero_right (n : nat) : n * zero = zero
diff --git a/tests/lean/run/nat_bug6.lean b/tests/lean/run/nat_bug6.lean
index eb0ddff80..7279386a0 100644
--- a/tests/lean/run/nat_bug6.lean
+++ b/tests/lean/run/nat_bug6.lean
@@ -7,9 +7,9 @@ succ : nat → nat
 
 namespace nat
 definition add (x y : nat) : nat := nat.rec x (λn r, succ r) y
-infixl `+`:65 := add
+infixl `+` := add
 definition mul (n m : nat) := nat.rec zero (fun m x, x + n) m
-infixl `*`:75 := mul
+infixl `*` := mul
 
 axiom mul_zero_right (n : nat) : n * zero = zero
 
diff --git a/tests/lean/run/nat_bug7.lean b/tests/lean/run/nat_bug7.lean
index d90a5f1a2..fb9a9ae0d 100644
--- a/tests/lean/run/nat_bug7.lean
+++ b/tests/lean/run/nat_bug7.lean
@@ -6,7 +6,7 @@ succ : nat → nat
 
 namespace nat
 definition add (x y : nat) : nat := nat.rec x (λn r, succ r) y
-infixl `+`:65 := add
+infixl `+` := add
 
 axiom add_right_comm (n m k : nat) : n + m + k = n + k + m
 open eq
diff --git a/tests/lean/run/nat_coe.lean b/tests/lean/run/nat_coe.lean
index fbc90fb69..bdd89cf52 100644
--- a/tests/lean/run/nat_coe.lean
+++ b/tests/lean/run/nat_coe.lean
@@ -4,10 +4,10 @@ constant nat : Type.{1}
 constant int : Type.{1}
 
 constant nat_add : nat → nat → nat
-infixl `+`:65 := nat_add
+infixl `+` := nat_add
 
 constant int_add : int → int → int
-infixl `+`:65 := int_add
+infixl `+` := int_add
 
 constant of_nat : nat → int
 coercion of_nat
diff --git a/tests/lean/run/not_bug1.lean b/tests/lean/run/not_bug1.lean
index ae5c8f866..ca36c686e 100644
--- a/tests/lean/run/not_bug1.lean
+++ b/tests/lean/run/not_bug1.lean
@@ -5,7 +5,7 @@ constant list : Type.{1}
 constant nil  : list
 constant cons : bool → list → list
 
-infixr `::`:65 := cons
+infixr `::` := cons
 notation `[` l:(foldr `,` (h t, cons h t) nil `]`) := l
 
 check []
diff --git a/tests/lean/run/occurs_check_bug1.lean b/tests/lean/run/occurs_check_bug1.lean
index 47a50b1d8..11fdd9d0d 100644
--- a/tests/lean/run/occurs_check_bug1.lean
+++ b/tests/lean/run/occurs_check_bug1.lean
@@ -4,7 +4,7 @@ open nat prod
 open decidable
 
 constant modulo (x : ℕ) (y : ℕ) : ℕ
-infixl `mod`:70 := modulo
+infixl `mod` := modulo
 
 constant gcd_aux : ℕ × ℕ → ℕ
 
diff --git a/tests/lean/run/over_subst.lean b/tests/lean/run/over_subst.lean
index 93c9e9d3d..79365cfb0 100644
--- a/tests/lean/run/over_subst.lean
+++ b/tests/lean/run/over_subst.lean
@@ -5,8 +5,8 @@ constant nat : Type.{1}
 constant add : nat → nat → nat
 constant le : nat → nat → Prop
 constant one : nat
-infixl `+`:65 := add
-infix `≤`:50 := le
+infixl `+` := add
+infix `≤` := le
 axiom add_assoc (a b c : nat) : (a + b) + c = a + (b + c)
 axiom add_le_left {a b : nat} (H : a ≤ b) (c : nat) : c + a ≤ c + b
 end nat
@@ -16,12 +16,12 @@ constant int : Type.{1}
 constant add : int → int → int
 constant le : int → int → Prop
 constant one : int
-infixl `+`:65 := add
-infix `≤`:50  := le
+infixl `+` := add
+infix `≤`  := le
 axiom add_assoc (a b c : int) : (a + b) + c = a + (b + c)
 axiom add_le_left {a b : int} (H : a ≤ b) (c : int) : c + a ≤ c + b
 definition lt (a b : int) := a + one ≤ b
-infix `<`:50  := lt
+infix `<`  := lt
 end int
 
 open int
diff --git a/tests/lean/run/ppbeta.lean b/tests/lean/run/ppbeta.lean
index c7a905fb2..a387bf731 100644
--- a/tests/lean/run/ppbeta.lean
+++ b/tests/lean/run/ppbeta.lean
@@ -4,7 +4,7 @@ open [coercions] nat
 
 definition lt (a b : int) := int.le (int.add a 1) b
 infix `<`     := lt
-infixl `+`:65 := int.add
+infixl `+` := int.add
 
 theorem lt_add_succ2 (a : int) (n : nat) : a < a + nat.succ n :=
 int.le_intro (show a + 1 + n = a + nat.succ n, from sorry)
diff --git a/tests/lean/run/set.lean b/tests/lean/run/set.lean
index 307c97b24..da5048241 100644
--- a/tests/lean/run/set.lean
+++ b/tests/lean/run/set.lean
@@ -2,6 +2,6 @@ import logic
 open bool
 
 definition set {{T : Type}} := T → bool
-infix `∈`:50 := λx A, A x = tt
+infix `∈` := λx A, A x = tt
 
 check 1 ∈ (λ x, tt)
diff --git a/tests/lean/run/set2.lean b/tests/lean/run/set2.lean
index 4b0c3e3e3..d4eac8c54 100644
--- a/tests/lean/run/set2.lean
+++ b/tests/lean/run/set2.lean
@@ -5,7 +5,7 @@ namespace set
 
 definition set (T : Type) := T → bool
 definition mem {T : Type} (a : T) (s : set T) := s a = tt
-infix `∈`:50 := mem
+infix `∈` := mem
 
 section
   variable {T : Type}
diff --git a/tests/lean/run/sum_bug.lean b/tests/lean/run/sum_bug.lean
index 0fd288e16..41d5b13ef 100644
--- a/tests/lean/run/sum_bug.lean
+++ b/tests/lean/run/sum_bug.lean
@@ -10,8 +10,8 @@ inl : A → sum A B,
 inr : B → sum A B
 
 namespace sum
-
-infixr `+`:25 := sum
+reserve infixr `+`:25
+infixr `+` := sum
 
 definition rec_on {A B : Type} {C : (A + B) → Type} (s : A + B)
   (H1 : ∀a : A, C (inl B a)) (H2 : ∀b : B, C (inr A b)) : C s :=
diff --git a/tests/lean/run/tactic23.lean b/tests/lean/run/tactic23.lean
index 29947ef4c..15b24401b 100644
--- a/tests/lean/run/tactic23.lean
+++ b/tests/lean/run/tactic23.lean
@@ -8,7 +8,7 @@ succ : nat → nat
 namespace nat
 definition add (a b : nat) : nat
 := nat.rec a (λ n r, succ r) b
-infixl `+`:65 := add
+infixl `+` := add
 
 definition one := succ zero
 
diff --git a/tests/lean/slow/list_elab2.lean b/tests/lean/slow/list_elab2.lean
index 905d1c675..1d1d62509 100644
--- a/tests/lean/slow/list_elab2.lean
+++ b/tests/lean/slow/list_elab2.lean
@@ -27,7 +27,7 @@ namespace list
 -- Type
 -- ----
 
-infix `::` : 65 := cons
+infixr `::` := cons
 
 section
 
@@ -50,7 +50,7 @@ notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
 definition concat (s t : list T) : list T :=
 list.rec t (fun x : T, fun l : list T, fun u : list T, cons x u) s
 
-infixl `++` : 65 := concat
+infixl `++` := concat
 
 theorem nil_concat (t : list T) : nil ++ t = t := refl _
 
diff --git a/tests/lean/slow/nat_bug2.lean b/tests/lean/slow/nat_bug2.lean
index 1a108911d..05965db35 100644
--- a/tests/lean/slow/nat_bug2.lean
+++ b/tests/lean/slow/nat_bug2.lean
@@ -137,7 +137,7 @@ theorem sub_induction {P : ℕ → ℕ → Prop} (n m : ℕ) (H1 : ∀m, P 0 m)
 
 -------------------------------------------------- add
 definition add (x y : ℕ) : ℕ := plus x y
-infixl `+`:65 := add
+infixl `+` := add
 theorem add_zero_right (n : ℕ) : n + 0 = n
 theorem add_succ_right (n m : ℕ) : n + succ m = succ (n + m)
 ---------- comm, assoc
@@ -271,7 +271,7 @@ theorem induction_plus_one {P : ℕ → Prop} (a : ℕ) (H1 : P 0)
 -------------------------------------------------- mul
 
 definition mul (n m : ℕ) := nat.rec 0 (fun m x, x + n) m
-infixl `*`:75 := mul
+infixl `*` := mul
 
 theorem mul_zero_right (n:ℕ) : n * 0 = 0
 theorem mul_succ_right (n m:ℕ) : n * succ m = n * m + n
@@ -388,8 +388,8 @@ theorem mul_eq_zero {n m : ℕ} (H : n * m = 0) : n = 0 ∨ m = 0
 -------------------------------------------------- le
 
 definition le (n m:ℕ) : Prop := ∃k, n + k = m
-infix  `<=`:50 := le
-infix  `≤`:50  := le
+infix  `<=` := le
+infix  `≤`  := le
 
 theorem le_intro {n m k : ℕ} (H : n + k = m) : n ≤ m
 := exists_intro k H
@@ -658,7 +658,7 @@ theorem mul_le {n m k l : ℕ} (H1 : n ≤ k) (H2 : m ≤ l) : n * m ≤ k * l
 -------------------------------------------------- lt
 
 definition lt (n m : ℕ) := succ n ≤ m
-infix `<`:50 := lt
+infix `<` := lt
 
 theorem lt_intro {n m k : ℕ} (H : succ n + k = m) : n < m
 := le_intro H
@@ -672,11 +672,11 @@ theorem lt_intro2 (n m : ℕ) : n < n + succ m
 -------------------------------------------------- ge, gt
 
 definition ge (n m : ℕ) := m ≤ n
-infix `>=`:50 := ge
-infix `≥`:50  := ge
+infix `>=` := ge
+infix `≥`  := ge
 
 definition gt (n m : ℕ) := m < n
-infix `>`:50  := gt
+infix `>`  := gt
 
 ---------- basic facts
 
@@ -1068,7 +1068,7 @@ theorem mul_eq_one {n m : ℕ} (H : n * m = 1) : n = 1 ∧ m = 1
 -------------------------------------------------- sub
 
 definition sub (n m : ℕ) : ℕ := nat.rec n (fun m x, pred x) m
-infixl `-`:65 := sub
+infixl `-` := sub
 theorem sub_zero_right (n : ℕ) : n - 0 = n
 theorem sub_succ_right (n m : ℕ) : n - succ m = pred (n - m)
 
diff --git a/tests/lean/slow/nat_wo_hints.lean b/tests/lean/slow/nat_wo_hints.lean
index f1b9cb5e6..3f8af567a 100644
--- a/tests/lean/slow/nat_wo_hints.lean
+++ b/tests/lean/slow/nat_wo_hints.lean
@@ -132,7 +132,7 @@ theorem sub_induction {P : ℕ → ℕ → Prop} (n m : ℕ) (H1 : ∀m, P 0 m)
 
 -------------------------------------------------- add
 definition add (x y : ℕ) : ℕ := plus x y
-infixl `+`:65 := add
+infixl `+` := add
 theorem add_zero_right (n : ℕ) : n + 0 = n
 theorem add_succ_right (n m : ℕ) : n + succ m = succ (n + m)
 ---------- comm, assoc
@@ -266,7 +266,7 @@ theorem induction_plus_one {P : ℕ → Prop} (a : ℕ) (H1 : P 0)
 -------------------------------------------------- mul
 
 definition mul (n m : ℕ) := nat.rec 0 (fun m x, x + n) m
-infixl `*`:75 := mul
+infixl `*` := mul
 
 theorem mul_zero_right (n:ℕ) : n * 0 = 0
 theorem mul_succ_right (n m:ℕ) : n * succ m = n * m + n
@@ -383,8 +383,8 @@ theorem mul_eq_zero {n m : ℕ} (H : n * m = 0) : n = 0 ∨ m = 0
 -------------------------------------------------- le
 
 definition le (n m:ℕ) : Prop := ∃k, n + k = m
-infix  `<=`:50 := le
-infix  `≤`:50  := le
+infix  `<=` := le
+infix  `≤`  := le
 
 theorem le_intro {n m k : ℕ} (H : n + k = m) : n ≤ m
 := exists_intro k H
@@ -657,7 +657,7 @@ theorem mul_le {n m k l : ℕ} (H1 : n ≤ k) (H2 : m ≤ l) : n * m ≤ k * l
 -------------------------------------------------- lt
 
 definition lt (n m : ℕ) := succ n ≤ m
-infix `<`:50 := lt
+infix `<` := lt
 
 theorem lt_intro {n m k : ℕ} (H : succ n + k = m) : n < m
 := le_intro H
@@ -671,11 +671,11 @@ theorem lt_intro2 (n m : ℕ) : n < n + succ m
 -------------------------------------------------- ge, gt
 
 definition ge (n m : ℕ) := m ≤ n
-infix `>=`:50 := ge
-infix `≥`:50  := ge
+infix `>=` := ge
+infix `≥`  := ge
 
 definition gt (n m : ℕ) := m < n
-infix `>`:50  := gt
+infix `>`  := gt
 
 ---------- basic facts
 
@@ -1073,7 +1073,7 @@ theorem mul_eq_one {n m : ℕ} (H : n * m = 1) : n = 1 ∧ m = 1
 -------------------------------------------------- sub
 
 definition sub (n m : ℕ) : ℕ := nat.rec n (fun m x, pred x) m
-infixl `-`:65 := sub
+infixl `-` := sub
 theorem sub_zero_right (n : ℕ) : n - 0 = n
 theorem sub_succ_right (n m : ℕ) : n - succ m = pred (n - m)
 
diff --git a/tests/lean/slow/path_groupoids.lean b/tests/lean/slow/path_groupoids.lean
index 2ecc0087a..0cd26b60e 100644
--- a/tests/lean/slow/path_groupoids.lean
+++ b/tests/lean/slow/path_groupoids.lean
@@ -18,7 +18,7 @@ idpath : path a a
 definition idpath := @path.idpath
 infix `≈`:50 := path
 -- TODO: is this right?
-notation x `≈` y:50 `:>`:0 A:0 := @path A x y
+notation x `≈`:50 y `:>`:0 A:0 := @path A x y
 notation `idp`:max := idpath _     -- TODO: can we / should we use `1`?
 
 namespace path