feat(frontends/lean/notation_cmd): make the notation for setting precedence uniform

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

library/standard/logic.lean

@@ -40,8 +40,8 @@ theorem absurd_elim {a : Bool} (b : Bool) (H1 : a) (H2 : ¬ a) : b
 inductive and (a b : Bool) : Bool :=
 | and_intro : a → b → and a b
 
-infixr `/\` 35 := and
-infixr `∧`  35 := and
+infixr `/\`:35 := and
+infixr `∧`:35 := and
 
 theorem and_elim {a b c : Bool} (H1 : a → b → c) (H2 : a ∧ b) : c
 := and_rec H1 H2
@@ -56,8 +56,8 @@ inductive or (a b : Bool) : Bool :=
 | or_intro_left  : a → or a b
 | or_intro_right : b → or a b
 
-infixr `\/` 30 := or
-infixr `∨` 30 := or
+infixr `\/`:30 := or
+infixr `∨`:30 := or
 
 theorem or_elim {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c
 := or_rec H2 H3 H1
@@ -74,7 +74,7 @@ theorem or_flip {a b : Bool} (H : a ∨ b) : b ∨ a
 inductive eq {A : Type} (a : A) : A → Bool :=
 | refl : eq a a
 
-infix `=` 50 := eq
+infix `=`:50 := eq
 
 theorem subst {A : Type} {a b : A} {P : A → Bool} (H1 : a = b) (H2 : P a) : P b
 := eq_rec H2 H1
@@ -104,8 +104,8 @@ theorem not_congr {a b : Bool} (H : a = b) : (¬ a) = (¬ b)
 theorem eqmp {a b : Bool} (H1 : a = b) (H2 : a) : b
 := subst H1 H2
 
-infixl `<|` 100 := eqmp
-infixl `◂`  100 := eqmp
+infixl `<|`:100 := eqmp
+infixl `◂`:100 := eqmp
 
 theorem eqmpr {a b : Bool} (H1 : a = b) (H2 : b) : a
 := (symm H1) ◂ H2
@@ -126,7 +126,7 @@ theorem eq_imp_trans {a b c : Bool} (H1 : a = b) (H2 : b → c) : a → c
 := assume Ha, H2 (H1 ◂ Ha)
 
 definition ne {A : Type} (a b : A) := ¬ (a = b)
-infix `≠` 50 := ne
+infix `≠`:50 := ne
 
 theorem ne_intro {A : Type} {a b : A} (H : a = b → false) : a ≠ b
 := H
@@ -150,7 +150,7 @@ calc_trans eq_ne_trans
 calc_trans ne_eq_trans
 
 definition iff (a b : Bool) := (a → b) ∧ (b → a)
-infix `↔` 50 := iff
+infix `↔`:50 := iff
 
 theorem iff_intro {a b : Bool} (H1 : a → b) (H2 : b → a) : a ↔ b
 := and_intro H1 H2
@@ -214,7 +214,7 @@ theorem cast_eq {A : Type} (H : A = A) (a : A) : cast H a = a
 
 definition heq {A B : Type} (a : A) (b : B) := ∃ H, cast H a = b
 
-infixl `==` 50 := heq
+infixl `==`:50 := heq
 
 theorem heq_type_eq {A B : Type} {a : A} {b : B} (H : a == b) : A = B
 := exists_elim H (λ H Hw, H)

src/frontends/lean/notation_cmd.cpp

@@ -81,7 +81,11 @@ using notation::action;
 
 static std::pair<notation_entry, optional<token_entry>> parse_mixfix_notation(parser & p, mixfix_kind k, bool overload) {
     std::string tk = parse_symbol(p, "invalid notation declaration, quoted symbol or identifier expected");
-    optional<unsigned> prec = parse_optional_precedence(p);
+    optional<unsigned> prec;
+    if (p.curr_is_token(g_colon)) {
+        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) {

tests/lean/bug1.lean

@@ -1,6 +1,6 @@
 definition bool [inline] : Type.{1}           := Type.{0}
 definition and  [inline] (p q : bool) : bool  := ∀ c : bool, (p → q → c) → c
-infixl `∧` 25 := and
+infixl `∧`:25 := and
 
 variable a : bool
 

tests/lean/calc1.lean

@@ -1,12 +1,12 @@
 variable A : Type.{1}
 definition bool [inline] : Type.{1} := Type.{0}
 variable eq : A → A → bool
-infixl `=` 50 := eq
+infixl `=`:50 := eq
 axiom subst (P : A → bool) (a b : A) (H1 : a = b) (H2 : P a) : P b
 axiom eq_trans (a b c : A) (H1 : a = b) (H2 : b = c) : a = c
 axiom eq_refl (a : A) : a = a
 variable le : A → A → bool
-infixl `≤` 50 := le
+infixl `≤`:50 := le
 axiom le_trans (a b c : A) (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c
 axiom le_refl (a : A) : a ≤ a
 axiom eq_le_trans (a b c : A) (H1 : a = b) (H2 : b ≤ c) : a ≤ c
@@ -29,7 +29,7 @@ check calc a   = b : H1
            ... = e : H4
 
 variable lt : A → A → bool
-infixl `<` 50 := lt
+infixl `<`:50 := lt
 axiom lt_trans (a b c : A) (H1 : a < b) (H2 : b < c) : a < c
 axiom le_lt_trans (a b c : A) (H1 : a ≤ b) (H2 : b < c) : a < c
 axiom lt_le_trans (a b c : A) (H1 : a < b) (H2 : b ≤ c) : a < c
@@ -41,7 +41,7 @@ check calc b  ≤ c : H2
           ... < d : H5
 
 variable le2 : A → A → bool
-infixl `≤` 50 := le2
+infixl `≤`:50 := le2
 variable le2_trans (a b c : A) (H1 : le2 a b) (H2 : le2 b c) : le2 a c
 calc_trans le2_trans
 print raw calc b   ≤ c : H2

tests/lean/let1.lean

@@ -1,7 +1,7 @@
 -- Correct version
 check let bool [inline]              := Type.{0},
           and  [inline] (p q : bool) := ∀ c : bool, (p → q → c) → c,
-          infixl `∧` 25             := and,
+          infixl `∧`:25             := and,
           and_intro (p q : bool) (H1 : p) (H2 : q) : p ∧ q
               := λ (c : bool) (H : p → q → c), H H1 H2,
           and_elim_left  (p q : bool) (H : p ∧ q) : p
@@ -12,7 +12,7 @@ check let bool [inline]              := Type.{0},
 
 check let bool [inline]                := Type.{0},
           and  [inline] (p q : bool)   := ∀ c : bool, (p → q → c) → c,
-          infixl `∧` 25               := and,
+          infixl `∧`:25               := and,
           and_intro [fact] (p q : bool) (H1 : p) (H2 : q) : q ∧ p
               := λ (c : bool) (H : p → q → c), H H1 H2,
           and_elim_left  (p q : bool) (H : p ∧ q) : p

tests/lean/run/e1.lean

@@ -2,7 +2,7 @@ definition Bool [inline] : Type.{1} := Type.{0}
 variable eq : forall {A : Type}, A → A → Bool
 variable N : Type.{1}
 variables a b c : N
-infix `=` 50 := eq
+infix `=`:50 := eq
 check a = b
 
 variable f : Bool → N → N

tests/lean/run/e3.lean

@@ -11,7 +11,7 @@ definition eq {A : Type} (a b : A)
 
 check eq
 
-infix `=` 50 := eq
+infix `=`:50 := eq
 
 theorem refl {A : Type} (a : A) : a = a
 := λ P H, H

tests/lean/run/e4.lean

@@ -11,7 +11,7 @@ definition eq {A : Type} (a b : A)
 
 check eq
 
-infix `=` 50 := eq
+infix `=`:50 := eq
 
 theorem refl {A : Type} (a : A) : a = a
 := λ P H, H

tests/lean/run/e5.lean

@@ -11,7 +11,7 @@ definition eq {A : Type} (a b : A)
 
 check eq
 
-infix `=` 50 := eq
+infix `=`:50 := eq
 
 theorem refl {A : Type} (a : A) : a = a
 := λ P H, H

tests/lean/run/have6.lean

@@ -1,6 +1,6 @@
 abbreviation Bool : Type.{1} := Type.{0}
 variable and : Bool → Bool → Bool
-infixl `∧` 25 := and
+infixl `∧`:25 := and
 variable and_intro : forall (a b : Bool), a → b → a ∧ b
 variables a b c d : Bool
 axiom Ha : a

tests/lean/run/n3.lean

@@ -1,7 +1,7 @@
 definition Bool [inline] : Type.{1} := Type.{0}
 variable N : Type.{1}
 variable and : Bool → Bool → Bool
-infixr `∧` 35 := and
+infixr `∧`:35 := and
 variable le : N → N → Bool
 variable lt : N → N → Bool
 precedence `≤`:50

tests/lean/run/n4.lean

@@ -3,7 +3,7 @@ section
   variable N : Type.{1}
   variables a b c : N
   variable and : Bool → Bool → Bool
-  infixr `∧` 35 := and
+  infixr `∧`:35 := and
   variable le : N → N → Bool
   variable lt : N → N → Bool
   precedence `≤`:50

tests/lean/run/t9.lean

@@ -1,7 +1,7 @@
 definition bool [inline] : Type.{1} := Type.{0}
 definition and (p q : bool) : bool
 := ∀ c : bool, (p → q → c) →  c
-infixl `∧` 25 := and
+infixl `∧`:25 := and
 theorem and_intro (p q : bool) (H1 : p) (H2 : q) : p ∧ q
 := λ (c : bool) (H : p → q → c), H H1 H2
 theorem and_elim_left (p q : bool) (H : p ∧ q) : p

tests/lean/t10.lean

@@ -8,7 +8,7 @@ variable q : B
 variable x : N
 variable y : N
 variable z : N
-infixr `∧` 25 := and
+infixr `∧`:25 := and
 notation `if` c `then` t `else` e := ite c t e
 check if p ∧ q then f x else y
 check if p ∧ q then q else y

tests/lean/t14.lean

@@ -33,7 +33,7 @@ end
 
 namespace foo
   variable f : A → A → A
-  infix `*` 75 := f
+  infix `*`:75 := f
 end
 
 section