Def Mathlib.Meta.delabInf

Modification history

2025-11-19 06:07
Mathlib/Order/Notation.lean
chore: move Mathlib to the module system (#31786) …
Deleted Mathlib.Meta.delabInfView on Github →
2025-09-04 11:48
Mathlib/Order/Notation.lean
fix: respect pp options in delaboration of max/min notation (#29312) …
Modified Mathlib.Meta.delabInfView on Github →
2025-04-21 06:29
Mathlib/Order/Notation.lean
feat: don't delaborate to `⊔` or `⊓` if we have a `LinearOrder` (#23558) …
Added Mathlib.Meta.delabInfView on Github →