diff --git a/library/data/prod.lean b/library/data/prod.lean index 71ba33247..8644c36c8 100644 --- a/library/data/prod.lean +++ b/library/data/prod.lean @@ -26,8 +26,8 @@ namespace prod definition pr1 (p : prod A B) := rec (λ x y, x) p definition pr2 (p : prod A B) := rec (λ x y, y) p - notation `pr₁`:max := pr1 - notation `pr₂`:max := pr2 + notation `pr₁` := pr1 + notation `pr₂` := pr2 variables (a : A) (b : B) diff --git a/library/data/unit.lean b/library/data/unit.lean index 3de08a28f..fad608890 100644 --- a/library/data/unit.lean +++ b/library/data/unit.lean @@ -7,7 +7,7 @@ open decidable inductive unit : Type := star : unit namespace unit - notation `⋆`:max := star + notation `⋆` := star -- remove duplication? protected theorem equal (a b : unit) : a = b := diff --git a/library/general_notation.lean b/library/general_notation.lean index 79df60cb6..efd27d26f 100644 --- a/library/general_notation.lean +++ b/library/general_notation.lean @@ -40,9 +40,6 @@ precedence `▸`:75 -- infixr -- ### types and type constructors -precedence `ℕ`:max -precedence `ℤ`:max - precedence `⊎`:25 -- infixr precedence `×`:30 -- infixr @@ -69,7 +66,6 @@ precedence `||`:65 -- infixl -- ### set operations precedence `∈`:50 -precedence `∅`:max precedence `∩`:70 precedence `∪`:65 diff --git a/library/type.lean b/library/type.lean index ab6325ccb..52b45248d 100644 --- a/library/type.lean +++ b/library/type.lean @@ -2,9 +2,9 @@ -- Released under Apache 2.0 license as described in the file LICENSE. -- Authors: Leonardo de Moura -notation `Prop`:max := Type.{0} -notation `Type'`:max := Type.{_+1} -notation `Type₊`:max := Type.{_+1} -notation `Type₁`:max := Type.{1} -notation `Type₂`:max := Type.{2} -notation `Type₃`:max := Type.{3} +notation `Prop` := Type.{0} +notation `Type'` := Type.{_+1} +notation `Type₊` := Type.{_+1} +notation `Type₁` := Type.{1} +notation `Type₂` := Type.{2} +notation `Type₃` := Type.{3}