michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/data/prod): make the notation for tuples and product types consistent

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-13 06:48:37 -07:00
parent a26618e0f2
commit 5c1d5133dd
2 changed files with 6 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/data/prod.lean
View file

@ -15,7 +15,7 @@ inductive prod (A B : Type) : Type :=
definition pair := @prod.mk definition pair := @prod.mk
namespace prod namespace prod
infixr `×` := prod infixl `×` := prod
-- notation for n-ary tuples -- notation for n-ary tuples
notation `(` h `,` t:(foldl `,` (e r, prod.mk r e) h) `)` := t notation `(` h `,` t:(foldl `,` (e r, prod.mk r e) h) `)` := t

5
tests/lean/run/prod_notation.lean Normal file
View file

@ -0,0 +1,5 @@
import data.prod data.num
open prod
definition tst1 : num × Prop × num × Prop := (1, true, 2, false)
definition tst2 : num × num × num := (1, 2, 3)