From 1864fc2f6c87cae6a2186e04a457e647384aa66b Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Thu, 28 Aug 2014 16:13:04 -0400
Subject: [PATCH] refactor(library): move more notation to general_notation

---
 library/general_notation.lean | 7 ++++---
 library/hott/equiv.lean       | 2 +-
 library/hott/path.lean        | 6 +++---
 3 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/library/general_notation.lean b/library/general_notation.lean
index f3c89026d..297951c53 100644
--- a/library/general_notation.lean
+++ b/library/general_notation.lean
@@ -32,6 +32,9 @@ precedence `=`:50
 precedence `≠`:50
 precedence `rfl`:max   -- shorthand for reflexivity
 
+precedence `≈`:50      -- used for path in hott
+precedence `∼`:50
+
 precedence `⁻¹`:100
 precedence `⬝`:75      -- infixr
 precedence `▸`:75      -- infixr
@@ -74,8 +77,6 @@ precedence `∪`:65
 
 -- ### other symbols
 
--- uncomment when inductive type syntax has changed
-
 precedence `|`:55     -- used for absolute value, subtypes, divisibility
 precedence `++`:65    -- list append
-precedence `::`:65    -- list cons
\ No newline at end of file
+precedence `::`:65    -- list cons
diff --git a/library/hott/equiv.lean b/library/hott/equiv.lean
index 4dd373046..e2caebce8 100644
--- a/library/hott/equiv.lean
+++ b/library/hott/equiv.lean
@@ -58,4 +58,4 @@ Equiv_rec (λequiv_fun equiv_isequiv, equiv_isequiv) e
 
 -- TODO: better symbol
 infix `<~>`:25 := Equiv
-notation e `⁻¹`:75 := equiv_inv e
+notation e `⁻¹` := equiv_inv e
diff --git a/library/hott/path.lean b/library/hott/path.lean
index c820c6dd2..7d667f641 100644
--- a/library/hott/path.lean
+++ b/library/hott/path.lean
@@ -18,7 +18,7 @@ using function
 inductive path {A : Type} (a : A) : A → Type :=
 idpath : path a a
 
-infix `≈`:50 := path
+infix `≈` := path
 notation x `≈` y:50 `:>`:0 A:0 := @path A x y    -- TODO: is this right?
 notation `idp`:max := idpath _    -- TODO: can we / should we use `1`?
 
@@ -206,7 +206,7 @@ abbreviation ap01 := ap
 abbreviation pointwise_paths {A : Type} {P : A → Type} (f g : Πx, P x) : Type :=
 Πx : A, f x ≈ g x
 
-infix `∼`:50 := pointwise_paths
+infix `∼` := pointwise_paths
 
 definition apD10 {A} {B : A → Type} {f g : Πx, B x} (H : f ≈ g) : f ∼ g :=
 λx, path.induction_on H idp
@@ -691,4 +691,4 @@ Hint Rewrite
 Ltac hott_simpl :=
   autorewrite with paths in * |- * ; auto with path_hints.
 
--/
\ No newline at end of file
+-/