diff --git a/library/init/prod.lean b/library/init/prod.lean index 1bcd76bdb2..a4970fed96 100644 --- a/library/init/prod.lean +++ b/library/init/prod.lean @@ -10,7 +10,7 @@ attribute [constructor] definition pair := @prod.mk notation A × B := prod A B -- notation for n-ary tuples -notation `(` h `, ` t:(foldl `, ` (e r, prod.mk r e) h) `)` := t +notation `(` h `, ` t:(foldr `, ` (e r, prod.mk e r)) `)` := prod.mk h t namespace prod notation `pr₁` := pr1 diff --git a/library/init/reserved_notation.lean b/library/init/reserved_notation.lean index 578cbe9eae..b4914770f0 100644 --- a/library/init/reserved_notation.lean +++ b/library/init/reserved_notation.lean @@ -170,8 +170,8 @@ reserve infixr ` ▹ `:75 /- types and type constructors -/ -reserve infixl ` ⊎ `:25 -reserve infixl ` × `:30 +reserve infixr ` ⊕ `:25 +reserve infixr ` × `:30 /- arithmetic operations -/