From 414ba28cef96a498eae5dcaf0d671d36c00c46ff Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 23 Mar 2025 12:36:13 -0700 Subject: [PATCH] fix: make pretty printed structure instances hoverable (#7648) This PR fixes a bug introduced in #7589, causing pretty printed structure instances to not be hoverable in the Infoview. This was caused by a choice node being introduced, since `{ $fields,* }` is ambiguous syntax. --- src/Lean/PrettyPrinter/Delaborator/Builtins.lean | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index 52350a98c4..50f83ed2e8 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -671,11 +671,9 @@ def delabStructureInstance : Delab := do paramMap := paramMap.insert (← x.fvarId!.getUserName) param return paramMap let (_, fields) ← collectStructFields s.induct paramMap #[] {} s - if ← withType <| getPPOption getPPStructureInstanceType then - let tyStx ← withType delab - `({ $fields,* : $tyStx }) - else - `({ $fields,* }) + let tyStx? : Option Term ← withType do + if ← getPPOption getPPStructureInstanceType then delab else pure none + `({ $fields,* $[: $tyStx?]? }) /-- State for `delabAppMatch` and helpers. -/