Def Lean.PrettyPrinter.Delaborator.SubExpr.withBindingBody'

Modification history

2024-05-02 13:42

Mathlib/Lean/PrettyPrinter/Delaborator.lean

chore: move to v4.8.0-rc1 (#12548) …

Deleted Lean.PrettyPrinter.Delaborator.SubExpr.withBindingBody'View on Github →

2023-10-26 01:32

Mathlib/Lean/PrettyPrinter/Delaborator.lean

feat: have `notation3` use elaborator when generating matchers, add support for pi/lambda (#6833) …

Added Lean.PrettyPrinter.Delaborator.SubExpr.withBindingBody'View on Github →