From 6c7e23ecaa615cc65b30066bd180398a32931f08 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 21 Oct 2014 14:08:07 -0700
Subject: [PATCH] refactor(library): use 'reserve' notation in the standard
 library

---
 library/algebra/category/morphism.lean |  2 +-
 library/data/bool.lean                 |  4 +-
 library/data/int/basic.lean            |  6 +-
 library/data/int/order.lean            | 12 ++--
 library/data/list/basic.lean           |  6 +-
 library/data/nat/basic.lean            |  4 +-
 library/data/nat/div.lean              |  4 +-
 library/data/nat/order.lean            | 12 ++--
 library/data/nat/sub.lean              |  2 +-
 library/data/num.lean                  |  8 +--
 library/data/prod.lean                 |  4 +-
 library/data/set.lean                  |  8 +--
 library/data/sum.lean                  |  2 +-
 library/data/vector.lean               |  4 +-
 library/general_notation.lean          | 76 ++++++++++++--------------
 library/hott/equiv.lean                |  2 +-
 library/hott/path.lean                 |  4 +-
 library/logic/connectives.lean         | 12 ++--
 library/logic/eq.lean                  | 12 ++--
 library/logic/instances.lean           |  6 +-
 tests/lean/run/abs.lean                |  2 +-
 21 files changed, 94 insertions(+), 98 deletions(-)

diff --git a/library/algebra/category/morphism.lean b/library/algebra/category/morphism.lean
index 9bbe04339..8c88abe54 100644
--- a/library/algebra/category/morphism.lean
+++ b/library/algebra/category/morphism.lean
@@ -24,7 +24,7 @@ namespace morphism
   definition inverse       (f : hom a b) [H : is_iso f] : hom b a :=
   is_iso.rec (λg h1 h2, g) H
 
-  postfix `⁻¹` := inverse
+  notation H ⁻¹ := inverse H
 
   theorem inverse_compose (f : hom a b) [H : is_iso f] : f⁻¹ ∘ f = id :=
   is_iso.rec (λg h1 h2, h1) H
diff --git a/library/data/bool.lean b/library/data/bool.lean
index eda3725cc..89c9d1f5c 100644
--- a/library/data/bool.lean
+++ b/library/data/bool.lean
@@ -41,7 +41,7 @@ namespace bool
   theorem bor.tt_left (a : bool) : bor tt a = tt :=
   rfl
 
-  infixl `||` := bor
+  notation a || b := bor a b
 
   theorem bor.tt_right (a : bool) : a || tt = tt :=
   cases_on a rfl rfl
@@ -78,7 +78,7 @@ namespace bool
   definition band (a b : bool) :=
   rec_on a ff (rec_on b ff tt)
 
-  infixl `&&` := band
+  notation a && b := band a b
 
   theorem band.ff_left (a : bool) : ff && a = ff :=
   rfl
diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index 8d6e89710..295ec4bf1 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -373,7 +373,7 @@ calc
     ... = pr2 (map_pair2 add a b) + pr1 (map_pair2 add a' b') : by simp
 
 definition add : ℤ → ℤ → ℤ := quotient_map_binary quotient (map_pair2 nat.add)
-infixl `+` := int.add
+notation a + b := int.add a b
 
 theorem add_comp (n m k l : ℕ) : psub (pair n m) + psub (pair k l) = psub (pair (n + k) (m + l)) :=
 have H : ∀a b, psub a + psub b = psub (map_pair2 nat.add a b),
@@ -442,7 +442,7 @@ by simp
 
 -- ## sub
 definition sub (a b : ℤ) : ℤ := a + -b
-infixl `-` := int.sub
+notation a - b := int.sub a b
 
 theorem sub_def (a b : ℤ) : a - b = a + -b :=
 rfl
@@ -607,7 +607,7 @@ calc
 definition mul : ℤ → ℤ → ℤ := quotient_map_binary quotient
   (fun u v : ℕ × ℕ, pair (pr1 u * pr1 v + pr2 u * pr2 v) (pr1 u * pr2 v + pr2 u * pr1 v))
 
-infixl `*` := int.mul
+notation a * b := int.mul a b
 
 theorem mul_comp (n m k l : ℕ) :
   psub (pair n m) * psub (pair k l) = psub (pair (n * k + m * l) (n * l + m * k)) :=
diff --git a/library/data/int/order.lean b/library/data/int/order.lean
index 66065552d..c67de322a 100644
--- a/library/data/int/order.lean
+++ b/library/data/int/order.lean
@@ -18,8 +18,8 @@ namespace int
 
 -- ## le
 definition le (a b : ℤ) : Prop := ∃n : ℕ, a + n = b
-infix  `<=` := int.le
-infix  `≤`  := int.le
+notation a <= b := int.le a b
+notation a ≤ b  := int.le a b
 
 theorem le_intro {a b : ℤ} {n : ℕ} (H : a + n = b) : a ≤ b :=
 exists_intro n H
@@ -180,14 +180,14 @@ iff.intro
 -- ----------------------------------------------
 
 definition lt (a b : ℤ) := a + 1 ≤ b
-infix `<`  := int.lt
+notation a < b  := int.lt a b
 
 definition ge (a b : ℤ) := b ≤ a
-infix `>=` := int.ge
-infix `≥`  := int.ge
+notation a >= b := int.ge a b
+notation a ≥ b  := int.ge a b
 
 definition gt (a b : ℤ) := b < a
-infix `>`  := int.gt
+notation a > b  := int.gt a b
 
 theorem lt_def (a b : ℤ) : a < b ↔ a + 1 ≤ b :=
 iff.refl (a < b)
diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index bf762858f..c0c947d3d 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -16,7 +16,7 @@ nil {} : list T,
 cons   : T → list T → list T
 
 namespace list
-infixr `::` := cons
+notation h :: t  := cons h t
 notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
 
 variable {T : Type}
@@ -39,7 +39,7 @@ protected definition rec_on {A : Type} {C : list A → Type} (l : list A)
 definition append (s t : list T) : list T :=
 rec t (λx l u, x::u) s
 
-infixl `++` : 65 := append
+notation l₁ ++ l₂ := append l₁ l₂
 
 theorem append.nil_left (t : list T) : nil ++ t = t
 
@@ -144,7 +144,7 @@ cases_on l
 definition mem (x : T) : list T → Prop :=
 rec false (λy l H, x = y ∨ H)
 
-infix `∈` := mem
+notation e ∈ s := mem e s
 
 theorem mem.nil (x : T) : x ∈ nil ↔ false :=
 iff.rfl
diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean
index d7870783e..fa5d2b829 100644
--- a/library/data/nat/basic.lean
+++ b/library/data/nat/basic.lean
@@ -45,7 +45,7 @@ inhabited.mk zero
 
 definition add (x y : ℕ) : ℕ :=
 nat.rec x (λ n r, succ r) y
-infixl `+` := add
+notation a + b := add a b
 
 definition of_num [coercion] [reducible] (n : num) : ℕ :=
 num.rec zero
@@ -255,7 +255,7 @@ nat.rec H1 (take n IH, !add.one ▸ (H2 n IH)) a
 -- --------------
 
 definition mul (n m : ℕ) := nat.rec 0 (fun m x, x + n) m
-infixl `*` := mul
+notation a * b := mul a b
 
 theorem mul.zero_right (n : ℕ) : n * 0 = 0
 
diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean
index a633584e5..34bf4dd49 100644
--- a/library/data/nat/div.lean
+++ b/library/data/nat/div.lean
@@ -180,7 +180,7 @@ rec_measure_spec (div_aux_rec y) (div_aux_decreasing y) x
 
 definition idivide (x : ℕ) (y : ℕ) : ℕ := div_aux y x
 
-infixl `div` := idivide
+notation a div b := idivide a b
 
 theorem div_zero {x : ℕ} : x div 0 = 0 :=
 div_aux_spec _ _ ⬝ if_pos (or.inl rfl)
@@ -256,7 +256,7 @@ rec_measure_spec (mod_aux_rec y) (mod_aux_decreasing y) x
 
 definition modulo (x : ℕ) (y : ℕ) : ℕ := mod_aux y x
 
-infixl `mod` := modulo
+notation a mod b := modulo a b
 
 theorem mod_zero {x : ℕ} : x mod 0 = x :=
 mod_aux_spec _ _ ⬝ if_pos (or.inl rfl)
diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean
index a5fe4128e..a1f4ce8aa 100644
--- a/library/data/nat/order.lean
+++ b/library/data/nat/order.lean
@@ -21,8 +21,8 @@ namespace nat
 
 definition le (n m : ℕ) : Prop := exists k : nat, n + k = m
 
-infix  `<=` := le
-infix  `≤`  := le
+notation a <= b := le a b
+notation a ≤ b  := le a b
 
 theorem le_intro {n m k : ℕ} (H : n + k = m) : n ≤ m :=
 exists_intro k H
@@ -256,14 +256,14 @@ general n
 -- ge and gt will be transparent, so we don't need to reprove theorems for le and lt for them
 
 definition lt (n m : ℕ) := succ n ≤ m
-infix `<` := lt
+notation a < b := lt a b
 
 definition ge (n m : ℕ) := m ≤ n
-infix `>=` := ge
-infix `≥` := ge
+notation a >= b := ge a b
+notation a ≥ b := ge a b
 
 definition gt (n m : ℕ) := m < n
-infix `>` := gt
+notation a > b := gt a b
 
 theorem lt_def (n m : ℕ) : (n < m) = (succ n ≤ m) := rfl
 
diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean
index c43aac1eb..307659b4f 100644
--- a/library/data/nat/sub.lean
+++ b/library/data/nat/sub.lean
@@ -20,7 +20,7 @@ namespace nat
 -- -----------
 
 definition sub (n m : ℕ) : nat := rec n (fun m x, pred x) m
-infixl `-` := sub
+notation a - b := sub a b
 
 theorem sub_zero_right (n : ℕ) : n - 0 = n
 
diff --git a/library/data/num.lean b/library/data/num.lean
index 014b28c3b..4a5350b5f 100644
--- a/library/data/num.lean
+++ b/library/data/num.lean
@@ -64,7 +64,7 @@ namespace pos_num
       (λm r, bit0 (f m)))
     b
 
-  infixl `+` := add
+  notation a + b := add a b
 
   section
   variables (a b : pos_num)
@@ -103,7 +103,7 @@ namespace pos_num
     (λn r, bit0 r + b)
     (λn r, bit0 r)
 
-  infixl `*` := mul
+  notation a * b := mul a b
 
   theorem mul.one_left (a : pos_num) : one * a = a :=
   rfl
@@ -161,6 +161,6 @@ namespace num
   definition mul (a b : num) : num :=
   rec_on a zero (λp_a, rec_on b zero (λp_b, pos (pos_num.mul p_a p_b)))
 
-  infixl `+` := add
-  infixl `*` := mul
+  notation a + b := add a b
+  notation a * b := mul a b
 end num
diff --git a/library/data/prod.lean b/library/data/prod.lean
index 8644c36c8..b32a8c247 100644
--- a/library/data/prod.lean
+++ b/library/data/prod.lean
@@ -1,7 +1,7 @@
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura, Jeremy Avigad
-import logic.inhabited logic.eq logic.decidable
+import logic.inhabited logic.eq logic.decidable general_notation
 
 -- data.prod
 -- =========
@@ -15,7 +15,7 @@ inductive prod (A B : Type) : Type :=
 definition pair := @prod.mk
 
 namespace prod
-  infixl `×` := prod
+  notation A × B := prod A B
 
   -- notation for n-ary tuples
   notation `(` h `,` t:(foldl `,` (e r, prod.mk r e) h) `)` := t
diff --git a/library/data/set.lean b/library/data/set.lean
index b18df00cf..24b5226b3 100644
--- a/library/data/set.lean
+++ b/library/data/set.lean
@@ -11,11 +11,11 @@ definition set (T : Type) :=
 T → bool
 definition mem {T : Type} (x : T) (s : set T) :=
 (s x) = tt
-infix `∈` := mem
+notation e ∈ s := mem e s
 
 definition eqv {T : Type} (A B : set T) : Prop :=
 ∀x, x ∈ A ↔ x ∈ B
-infixl `∼`:50 := eqv
+notation a ∼ b := eqv a b
 
 theorem eqv_refl {T : Type} (A : set T) : A ∼ A :=
 take x, iff.rfl
@@ -41,7 +41,7 @@ rfl
 
 definition inter {T : Type} (A B : set T) : set T :=
 λx, A x && B x
-infixl `∩` := inter
+notation a ∩ b := inter a b
 
 theorem mem_inter {T : Type} (x : T) (A B : set T) : x ∈ A ∩ B ↔ (x ∈ A ∧ x ∈ B) :=
 iff.intro
@@ -68,7 +68,7 @@ take x, band.assoc (A x) (B x) (C x) ▸ iff.rfl
 
 definition union {T : Type} (A B : set T) : set T :=
 λx, A x || B x
-infixl `∪` := union
+notation a ∪ b := union a b
 
 theorem mem_union {T : Type} (x : T) (A B : set T) : x ∈ A ∪ B ↔ (x ∈ A ∨ x ∈ B) :=
 iff.intro
diff --git a/library/data/sum.lean b/library/data/sum.lean
index 44d3189b4..12d9a79a9 100644
--- a/library/data/sum.lean
+++ b/library/data/sum.lean
@@ -12,7 +12,7 @@ inductive sum (A B : Type) : Type :=
   inr : B → sum A B
 
 namespace sum
-  infixr `⊎` := sum
+  notation A ⊎ B := sum A B
   namespace extra_notation
     infixr `+`:25 := sum    -- conflicts with notation for addition
   end extra_notation
diff --git a/library/data/vector.lean b/library/data/vector.lean
index be6d89059..d8566e1e5 100644
--- a/library/data/vector.lean
+++ b/library/data/vector.lean
@@ -9,7 +9,7 @@ inductive vector (T : Type) : ℕ → Type :=
   cons : T → ∀{n}, vector T n → vector T (succ n)
 
 namespace vector
-  infix `::` := cons --at what level?
+  notation a :: b := cons a b
   notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
 
   section sc_vector
@@ -322,5 +322,5 @@ namespace vector
 -- theorem nth_succ (x0 : T) (l : list T) (n : ℕ) : nth x0 l (succ n) = nth x0 (tail l) n := refl _
 
   end sc_vector
-  infixl `++`:65 := concat
+  notation a ++ b := concat a b
 end vector
diff --git a/library/general_notation.lean b/library/general_notation.lean
index efd27d26f..b1ebfb0dd 100644
--- a/library/general_notation.lean
+++ b/library/general_notation.lean
@@ -11,7 +11,6 @@
 notation `assume` binders `,` r:(scoped f, f) := r
 notation `take`   binders `,` r:(scoped f, f) := r
 
-
 -- Global declarations of right binding strength
 -- ---------------------------------------------
 
@@ -19,58 +18,55 @@ notation `take`   binders `,` r:(scoped f, f) := r
 -- conventions.
 
 -- ### Logical operations and relations
+reserve prefix `¬`:40
+reserve infixr `∧`:35
+reserve infixr `/\`:35
+reserve infixr `‌\/`:30
+reserve infixr `∨`:30
+reserve infix `<->`:25
+reserve infix `↔`:25
+reserve infix `=`:50
+reserve infix `≠`:50
+reserve infix `≈`:50
+reserve infix `∼`:50
 
-precedence `¬`:40
-precedence `/\`:35    -- infixr
-precedence `∧`:35     -- infixr
-precedence `\/`:30    -- infixr
-precedence `∨`:30     -- infixr
-precedence `<->`:25
-precedence `↔`:25
-
-precedence `=`:50
-precedence `≠`:50
-
-precedence `≈`:50      -- used for path in hott
-precedence `∼`:50
-
-precedence `⁻¹`:100
-precedence `⬝`:75      -- infixr
-precedence `▸`:75      -- infixr
+reserve postfix `⁻¹`:100
+reserve infixr `⬝`:75
+reserve infixr `▸`:75
 
 -- ### types and type constructors
 
-precedence `⊎`:25      -- infixr
-precedence `×`:30      -- infixr
+reserve infixl `⊎`:25
+reserve infixl `×`:30
 
 -- ### arithmetic operations
 
-precedence `+`:65      -- infixl
-precedence `-`:65      -- infixl; for negation, follow by rbp 100
-precedence `*`:70      -- infixl
-precedence `div`:70    -- infixl
-precedence `mod`:70    -- infixl
+reserve infixl `+`:65
+reserve infixl `-`:65
+reserve infixl `*`:70
+reserve infixl `div`:70
+reserve infixl `mod`:70
 
-precedence `<=`:50
-precedence `≤`:50
-precedence `<`:50
-precedence `>=`:50
-precedence `≥`:50
-precedence `>`:50
+reserve infix `<=`:50
+reserve infix `≤`:50
+reserve infix `<`:50
+reserve infix `>=`:50
+reserve infix `≥`:50
+reserve infix `>`:50
 
 -- ### boolean operations
 
-precedence `&&`:70     -- infixl
-precedence `||`:65     -- infixl
+reserve infixl `&&`:70
+reserve infixl `||`:65
 
 -- ### set operations
 
-precedence `∈`:50
-precedence `∩`:70
-precedence `∪`:65
+reserve infix `∈`:50
+reserve infixl `∩`:70
+reserve infixl `∪`:65
 
 -- ### other symbols
-
-precedence `|`:55     -- used for absolute value, subtypes, divisibility
-precedence `++`:65    -- list append
-precedence `::`:65    -- list cons
+precedence `|`:55
+reserve notation | a:55 |
+reserve infixl `++`:65
+reserve infixr `::`:65
diff --git a/library/hott/equiv.lean b/library/hott/equiv.lean
index 8c531013a..034f46484 100644
--- a/library/hott/equiv.lean
+++ b/library/hott/equiv.lean
@@ -53,4 +53,4 @@ Equiv.rec (λequiv_fun equiv_isequiv, equiv_isequiv) e
 
 -- TODO: better symbol
 infix `<~>`:25 := Equiv
-notation e `⁻¹` := equiv_inv e
+notation H ⁻¹ := equiv_inv H
diff --git a/library/hott/path.lean b/library/hott/path.lean
index f65dfd55e..6528e5f6f 100644
--- a/library/hott/path.lean
+++ b/library/hott/path.lean
@@ -19,8 +19,8 @@ inductive path {A : Type} (a : A) : A → Type :=
 idpath : path a a
 
 namespace path
-infix `≈` := path
-notation x `≈` y:50 `:>`:0 A:0 := @path A x y    -- TODO: is this right?
+notation a ≈ b := path a b
+notation x ≈ y `:>`:50 A:49 := @path A x y
 definition idp {A : Type} {a : A} := idpath a
 
 protected definition induction_on {A : Type} {a b : A} (p : a ≈ b)
diff --git a/library/logic/connectives.lean b/library/logic/connectives.lean
index 189e85503..cdf727a17 100644
--- a/library/logic/connectives.lean
+++ b/library/logic/connectives.lean
@@ -9,8 +9,8 @@ import general_notation .eq
 inductive and (a b : Prop) : Prop :=
   intro : a → b → and a b
 
-infixr `/\` := and
-infixr `∧` := and
+notation a /\ b := and a b
+notation a ∧ b  := and a b
 
 variables {a b c d : Prop}
 
@@ -49,8 +49,8 @@ inductive or (a b : Prop) : Prop :=
   intro_left  : a → or a b,
   intro_right : b → or a b
 
-infixr `\/` := or
-infixr `∨` := or
+notation a `\/` b := or a b
+notation a ∨ b := or a b
 
 namespace or
   theorem inl (Ha : a) : a ∨ b :=
@@ -105,8 +105,8 @@ assume not_em : ¬(p ∨ ¬p),
 -- ---
 definition iff (a b : Prop) := (a → b) ∧ (b → a)
 
-infix `<->` := iff
-infix `↔` := iff
+notation a <-> b := iff a b
+notation a ↔ b := iff a b
 
 namespace iff
   theorem def : (a ↔ b) = ((a → b) ∧ (b → a)) :=
diff --git a/library/logic/eq.lean b/library/logic/eq.lean
index cdee94207..eaf9e1606 100644
--- a/library/logic/eq.lean
+++ b/library/logic/eq.lean
@@ -1,7 +1,7 @@
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
-import .prop
+import general_notation .prop
 
 -- logic.eq
 -- ====================
@@ -14,7 +14,7 @@ import .prop
 inductive eq {A : Type} (a : A) : A → Prop :=
 refl : eq a a
 
-infix `=` := eq
+notation a = b := eq a b
 definition rfl {A : Type} {a : A} := eq.refl a
 
 -- proof irrelevance is built in
@@ -40,9 +40,9 @@ namespace eq
   subst H (refl a)
 
   namespace ops
-    postfix `⁻¹` := symm
-    infixr `⬝`   := trans
-    infixr `▸`   := subst
+    notation H `⁻¹` := symm H
+    notation H1 ⬝ H2 := trans H1 H2
+    notation H1 ▸ H2 := subst H1 H2
  end ops
 end eq
 
@@ -201,7 +201,7 @@ end
 -- --
 
 definition ne {A : Type} (a b : A) := ¬(a = b)
-infix `≠` := ne
+notation a ≠ b := ne a b
 
 namespace ne
   variable {A : Type}
diff --git a/library/logic/instances.lean b/library/logic/instances.lean
index 30cb9779a..a3eeedcea 100644
--- a/library/logic/instances.lean
+++ b/library/logic/instances.lean
@@ -124,9 +124,9 @@ end iff
 calc_subst iff.subst
 
 namespace iff_ops
-  postfix `⁻¹`:100   := iff.symm
-  infixr `⬝`:75      := iff.trans
-  infixr `▸`:75      := iff.subst
+  notation H ⁻¹ := iff.symm H
+  notation H1 ⬝ H2 := iff.trans H1 H2
+  notation H1 ▸ H2 := iff.subst H1 H2
   definition refl  := iff.refl
   definition symm  := @iff.symm
   definition trans := @iff.trans
diff --git a/tests/lean/run/abs.lean b/tests/lean/run/abs.lean
index 2654a18a2..209f5a47d 100644
--- a/tests/lean/run/abs.lean
+++ b/tests/lean/run/abs.lean
@@ -2,6 +2,6 @@ import data.int
 open int
 
 constant abs : int → int
-notation `|`:40 A:40 `|` := abs A
+notation `|` A `|` := abs A
 constants a b c : int
 check |a + |b| + c|