From db4d33487a0655df03c28799a64f8493bfa9512a Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@protonmail.com>
Date: Fri, 30 Jul 2021 13:41:36 -0700
Subject: [PATCH] fix: unexpanders can't specify exact names

---
 src/Init/NotationExtra.lean | 36 ++++++++++++++++++------------------
 1 file changed, 18 insertions(+), 18 deletions(-)

diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
index 949a1cb571..7c15a08b9a 100644
--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -94,56 +94,56 @@ macro:35 xs:bracketedExplicitBinders " × " b:term:35  : term => expandBrackedBi
 macro:35 xs:bracketedExplicitBinders " ×' " b:term:35 : term => expandBrackedBinders `PSigma xs b
 
 @[appUnexpander Unit.unit] def unexpandUnit : Lean.PrettyPrinter.Unexpander
-  | `(Unit.unit) => `(())
+  | `($(_)) => `(())
   | _            => throw ()
 
 @[appUnexpander List.nil] def unexpandListNil : Lean.PrettyPrinter.Unexpander
-  | `(List.nil) => `([])
-  | _           => throw ()
+  | `($(_)) => `([])
+  | _       => throw ()
 
 @[appUnexpander List.cons] def unexpandListCons : Lean.PrettyPrinter.Unexpander
-  | `(List.cons $x [])      => `([$x])
-  | `(List.cons $x [$xs,*]) => `([$x, $xs,*])
+  | `($(_) $x [])      => `([$x])
+  | `($(_) $x [$xs,*]) => `([$x, $xs,*])
   | _                       => throw ()
 
 @[appUnexpander List.toArray] def unexpandListToArray : Lean.PrettyPrinter.Unexpander
-  | `(List.toArray [$xs,*]) => `(#[$xs,*])
+  | `($(_) [$xs,*]) => `(#[$xs,*])
   | _                       => throw ()
 
 @[appUnexpander Prod.mk] def unexpandProdMk : Lean.PrettyPrinter.Unexpander
-  | `(Prod.mk $x ($y, $ys,*)) => `(($x, $y, $ys,*))
-  | `(Prod.mk $x $y)          => `(($x, $y))
+  | `($(_) $x ($y, $ys,*)) => `(($x, $y, $ys,*))
+  | `($(_) $x $y)          => `(($x, $y))
   | _                         => throw ()
 
 @[appUnexpander ite] def unexpandIte : Lean.PrettyPrinter.Unexpander
-  | `(ite $c $t $e) => `(if $c then $t else $e)
+  | `($(_) $c $t $e) => `(if $c then $t else $e)
   | _               => throw ()
 
 @[appUnexpander sorryAx] def unexpandSorryAx : Lean.PrettyPrinter.Unexpander
-  | `(sorryAx _)    => `(sorry)
-  | `(sorryAx _ $b) => `(sorry)
+  | `($(_) _)    => `(sorry)
+  | `($(_) _ $b) => `(sorry)
   | _               => throw ()
 
 @[appUnexpander Eq.ndrec] def unexpandEqNDRec : Lean.PrettyPrinter.Unexpander
-  | `(Eq.ndrec $m $h) => `($h ▸ $m)
+  | `($(_) $m $h) => `($h ▸ $m)
   | _                 => throw ()
 
 @[appUnexpander Eq.rec] def unexpandEqRec : Lean.PrettyPrinter.Unexpander
-  | `(Eq.rec $m $h) => `($h ▸ $m)
+  | `($(_) $m $h) => `($h ▸ $m)
   | _               => throw ()
 
 @[appUnexpander Exists] def unexpandExists : Lean.PrettyPrinter.Unexpander
-  | `(Exists fun $x:ident => ∃ $xs:binderIdent*, $b) => `(∃ $x:ident $xs:binderIdent*, $b)
-  | `(Exists fun $x:ident => $b)                     => `(∃ $x:ident, $b)
-  | `(Exists fun ($x:ident : $t) => $b)              => `(∃ ($x:ident : $t), $b)
+  | `($(_) fun $x:ident => ∃ $xs:binderIdent*, $b) => `(∃ $x:ident $xs:binderIdent*, $b)
+  | `($(_) fun $x:ident => $b)                     => `(∃ $x:ident, $b)
+  | `($(_) fun ($x:ident : $t) => $b)              => `(∃ ($x:ident : $t), $b)
   | _                                                => throw ()
 
 @[appUnexpander Sigma] def unexpandSigma : Lean.PrettyPrinter.Unexpander
-  | `(Sigma fun ($x:ident : $t) => $b) => `(($x:ident : $t) × $b)
+  | `($(_) fun ($x:ident : $t) => $b) => `(($x:ident : $t) × $b)
   | _                                  => throw ()
 
 @[appUnexpander PSigma] def unexpandPSigma : Lean.PrettyPrinter.Unexpander
-  | `(PSigma fun ($x:ident : $t) => $b) => `(($x:ident : $t) ×' $b)
+  | `($(_) fun ($x:ident : $t) => $b) => `(($x:ident : $t) ×' $b)
   | _                                   => throw ()
 
 syntax "funext " (colGt term:max)+ : tactic