From 9fe8e09f3017496a68f079acfd3801481ee7dc90 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 16 Aug 2016 10:34:32 -0700 Subject: [PATCH] feat(init/reserved_notation): product binds to the right --- library/init/prod.lean | 2 +- library/init/reserved_notation.lean | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) 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 -/