Def Lean.PrettyPrinter.Delaborator.withBindingBodyUnusedName'

Modification history

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.withBindingBodyUnusedName'View on Github →