diff --git a/library/data/prod.lean b/library/data/prod.lean index 9994c5a7a..71ba33247 100644 --- a/library/data/prod.lean +++ b/library/data/prod.lean @@ -15,7 +15,7 @@ inductive prod (A B : Type) : Type := definition pair := @prod.mk namespace prod - infixr `×` := prod + infixl `×` := prod -- notation for n-ary tuples notation `(` h `,` t:(foldl `,` (e r, prod.mk r e) h) `)` := t diff --git a/tests/lean/run/prod_notation.lean b/tests/lean/run/prod_notation.lean new file mode 100644 index 000000000..7182963ad --- /dev/null +++ b/tests/lean/run/prod_notation.lean @@ -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)