From 5c1d5133dd37e4dc38d0bbed8fc6e0db63f1a42d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 13 Oct 2014 06:48:37 -0700 Subject: [PATCH] fix(library/data/prod): make the notation for tuples and product types consistent --- library/data/prod.lean | 2 +- tests/lean/run/prod_notation.lean | 5 +++++ 2 files changed, 6 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/prod_notation.lean diff --git a/library/data/prod.lean b/library/data/prod.lean index 9994c5a7af..71ba332476 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 0000000000..7182963ad5 --- /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)