From ae0daf9639ef35dc98434e133bb17e22c7cfca93 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 28 Nov 2014 23:02:19 -0800 Subject: [PATCH] fix(library/data/prod/decl): give preference to unicode version when pretty printing --- library/data/prod/decl.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/data/prod/decl.lean b/library/data/prod/decl.lean index 046dd00e8c..e7cd143aa8 100644 --- a/library/data/prod/decl.lean +++ b/library/data/prod/decl.lean @@ -14,8 +14,8 @@ mk :: (pr1 : A) (pr2 : B) definition pair := @prod.mk namespace prod - notation A × B := prod A B notation A * B := prod A B + notation A × B := prod A B namespace low_precedence_times reserve infixr `*`:30 -- conflicts with notation for multiplication infixr `*` := prod