Def Lean.PrettyPrinter.Delaborator.annotateGoToSyntaxDef

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.annotateGoToSyntaxDefView on Github →