Def Lean.PrettyPrinter.Delaborator.annotateGoToDef

Modification history

2025-04-21 06:29
Mathlib/Lean/PrettyPrinter/Delaborator.lean
feat: don't delaborate to `⊔` or `⊓` if we have a `LinearOrder` (#23558) …
Added Lean.PrettyPrinter.Delaborator.annotateGoToDefView on Github →