max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(init/reserved_notation): product binds to the right

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-16 10:34:32 -07:00
parent b0abea78b6
commit 9fe8e09f30
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/prod.lean
View file

@ -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

4
library/init/reserved_notation.lean
View file

@ -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 -/