From 94cc8eb863198badc00643454a31cb0a6a4208c4 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 16 Jul 2024 12:04:51 -0700 Subject: [PATCH] chore: add comment for why anonymous constructor notation isn't flattened during pretty printing (#4764) --- src/Lean/PrettyPrinter/Delaborator/Builtins.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index 18c8720a47c6..acabb4c3077a 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -199,6 +199,10 @@ def unexpandStructureInstance (stx : Syntax) : Delab := whenPPOption getPPStruct let mut fields := #[] guard $ fieldNames.size == stx[1].getNumArgs if hasPPUsingAnonymousConstructorAttribute env s.induct then + /- Note that we don't flatten anonymous constructor notation. Only a complete such notation receives TermInfo, + and flattening would cause the flattened-in notation to lose its TermInfo. + Potentially it would be justified to flatten anonymous constructor notation when the terms are + from the same type family (think `Sigma`), but for now users can write a custom delaborator in such instances. -/ return ← withTypeAscription (cond := (← withType <| getPPOption getPPStructureInstanceType)) do `(⟨$[$(stx[1].getArgs)],*⟩) let args := e.getAppArgs