From 9744b51c1bb9987e5f47864a14ea4e72f27882b7 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Thu, 29 Jul 2021 15:04:03 -0700 Subject: [PATCH] fix: unexpand pairs --- src/Init/NotationExtra.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean index 6328dfceb9..949a1cb571 100644 --- a/src/Init/NotationExtra.lean +++ b/src/Init/NotationExtra.lean @@ -111,9 +111,9 @@ macro:35 xs:bracketedExplicitBinders " ×' " b:term:35 : term => expandBrackedBi | _ => throw () @[appUnexpander Prod.mk] def unexpandProdMk : Lean.PrettyPrinter.Unexpander - | `(Prod.mk $x `(($y, $ys,*))) => `(($x, $y, $ys,*)) - | `(Prod.mk $x $y) => `(($x, $y)) - | _ => throw () + | `(Prod.mk $x ($y, $ys,*)) => `(($x, $y, $ys,*)) + | `(Prod.mk $x $y) => `(($x, $y)) + | _ => throw () @[appUnexpander ite] def unexpandIte : Lean.PrettyPrinter.Unexpander | `(ite $c $t $e) => `(if $c then $t else $e)