max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: pretty print .coeFun with terminfo of coercee (#6085)

Browse source 
This PR improves the term info for coercions marked with
`CoeFnType.coeFun` (such as `DFunLike.coe` in Mathlib), making "go to
definition" on the function name work. Hovering over such a coerced
function will show the coercee rather than the coercion expression. The
coercion expression can still be seen by hovering over the whitespace in
the function application.
This commit is contained in:
Kyle Miller 2024-11-14 17:45:38 -08:00 • committed by GitHub
parent e0d7c3ac79
commit 498d41633b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 20 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
src/Lean/PrettyPrinter/Delaborator/Builtins.lean
View file

@ -1092,19 +1092,29 @@ def coeDelaborator : Delab := whenPPOption getPPCoercions do
let e ← getExpr
let .const declName _ := e.getAppFn | failure
let some info ← Meta.getCoeFnInfo? declName | failure
let n := e.getAppNumArgs
guard <| n ≥ info.numArgs
if (← getPPOption getPPExplicit) && info.coercee != 0 then
-- Approximation: the only implicit arguments come before the coercee
failure
let n := e.getAppNumArgs
withOverApp info.numArgs do
match info.type with
| .coe => `(↑$(← withNaryArg info.coercee delab))
| .coeFun =>
if n = info.numArgs then
`(⇑$(← withNaryArg info.coercee delab))
else
withNaryArg info.coercee delab
| .coeSort => `(↥$(← withNaryArg info.coercee delab))
if n == info.numArgs then
delabHead info 0 false
else
let nargs := n - info.numArgs
delabAppCore nargs (delabHead info nargs) (unexpand := false)
where
delabHead (info : CoeFnInfo) (nargs : Nat) (insertExplicit : Bool) : Delab := do
guard <| !insertExplicit
if info.type == .coeFun && nargs > 0 then
-- In the CoeFun case, annotate with the coercee itself.
-- We can still see the whole coercion expression by hovering over the whitespace between the arguments.
withNaryArg info.coercee <| withAnnotateTermInfo delab
else
withAnnotateTermInfo do
match info.type with
| .coe => `(↑$(← withNaryArg info.coercee delab))
| .coeFun => `(⇑$(← withNaryArg info.coercee delab))
| .coeSort => `(↥$(← withNaryArg info.coercee delab))
@[builtin_delab app.dite]
def delabDIte : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPNotation <| withOverApp 5 do