From 89d897a34d64a5f286ff4c808ab36847dc50a7b5 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 2 Feb 2025 14:54:23 -0800 Subject: [PATCH] feat: make coeFun delaborator respect `pp.tagAppFns` (#6729) This PR makes the pretty printer for `.coeFun`-tagged functions respect `pp.tagAppFns`. The effect is that in docgen, when an expression pretty prints as `f x y z` with `f` a coerced function, then if `f` is a constant it will be linkified. --- src/Lean/PrettyPrinter/Delaborator/Builtins.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index 7567cff8da..87a7d4f011 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -1117,9 +1117,12 @@ where withTypeAscription (cond := ← getPPOption getPPCoercionsTypes) do guard <| !insertExplicit if info.type == .coeFun && nargs > 0 then - -- In the CoeFun case, annotate with the coercee itself. + -- In the `.coeFun` case, delaborate the coercee itself. -- We can still see the whole coercion expression by hovering over the whitespace between the arguments. - withNaryArg info.coercee <| withAnnotateTermInfo delab + -- In the `pp.tagAppFns` case, if the coercee is a constant application, + -- then `delab` will tag the result with the constant, ensuring docgen linkifies it. + let tagAppFns ← getPPOption getPPTagAppFns + withNaryArg info.coercee <| withOptionAtCurrPos `pp.tagAppFns tagAppFns delab else withAnnotateTermInfo do match info.type with