From d0700bc911cc231e06d64abe44121a14bdaed2a4 Mon Sep 17 00:00:00 2001
From: Chris Wong <lambda.fairy@gmail.com>
Date: Sun, 16 Feb 2025 16:42:24 +1100
Subject: [PATCH] Parentheses cannot be matched in unexpander

---
 lean/extra/03_pretty-printing.lean | 33 ++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)

diff --git a/lean/extra/03_pretty-printing.lean b/lean/extra/03_pretty-printing.lean
index b37431e..423c563 100644
--- a/lean/extra/03_pretty-printing.lean
+++ b/lean/extra/03_pretty-printing.lean
@@ -140,6 +140,39 @@ def unexpMyId : Unexpander
 For a few nice examples of unexpanders you can take a look at
 [NotationExtra](https://github.com/leanprover/lean4/blob/master/src/Init/NotationExtra.lean)
 
+### Handling nested parentheses
+
+Since the delaborator runs before the parenthesizer, the expression given to the unexpander lacks
+parentheses. This means that any pattern that has them will fail to match. For example, this
+unexpander fails:
+-/
+
+def removeId {α} (x : α) := x
+
+@[app_unexpander removeId]
+def unexpRemoveId : Unexpander
+  | `($_removeId (id $arg)) => pure arg
+  | _ => throw ()
+
+#check removeId (id 42) -- removeId (id 42) : Nat
+
+/-!
+We can work around this issue with a nested `match`:
+-/
+
+def removeId' {α} (x : α) := x
+
+@[app_unexpander removeId']
+def unexpRemoveId' : Unexpander
+  | `($_removeId' $arg) =>
+    match arg with
+      | `(id $arg) => pure arg
+      | _ => throw ()
+  | _ => throw ()
+
+#check removeId' (id 42) -- 42 : Nat
+
+/-!
 ### Mini project
 As per usual, we will tackle a little mini project at the end of the chapter.
 This time we build our own unexpander for a mini programming language.