feat(frontends/lean): validate infixl/infixr/postfix/prefix declarations against reserved notations

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

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}

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
 

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>();

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

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

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 _

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

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

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
 

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
 

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
 

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
 

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)

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}

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

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
 

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
 

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

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

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
 

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

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

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 []

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 : ℕ × ℕ → ℕ
 

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

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)

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)

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}

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 :=

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
 

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 _
 

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)
 

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)
 

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