feat(library/data/sum): use + notation for sum

library/data/sum.lean

@@ -1,8 +1,10 @@
 -- 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.prop logic.inhabited logic.decidable
 open inhabited decidable eq.ops
+
 -- data.sum
 -- ========
 -- The sum type, aka disjoint union.
@@ -12,11 +14,14 @@ inductive sum (A B : Type) : Type :=
   inr : B → sum A B
 
 namespace sum
+
   notation A ⊎ B := sum A B
-  namespace extra_notation
+  notation A + B := sum A B
+
+  namespace low_precedence_plus
     reserve infixr `+`:25 -- conflicts with notation for addition
     infixr `+` := sum
-  end extra_notation
+  end low_precedence_plus
 
   variables {A B : Type}
   variables {a a₁ a₂ : A} {b b₁ b₂ : B}