Additions to the delaborator #
def
Lean.PrettyPrinter.Delaborator.withBindingBodyUnusedName'
{α : Type}
(d : Lean.Syntax → Lean.Expr → Lean.PrettyPrinter.Delaborator.DelabM α)
:
Assuming the current expression in a lambda or pi,
descend into the body using an unused name generated from the binder's name.
Provides d with both Syntax for the bound name as an identifier
as well as the fresh fvar for the bound variable.
See also Lean.PrettyPrinter.Delaborator.withBindingBodyUnusedName.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.PrettyPrinter.Delaborator.OptionsPerPos.setBool
(opts : Lean.PrettyPrinter.Delaborator.OptionsPerPos)
(p : Lean.SubExpr.Pos)
(n : Lean.Name)
(v : Bool)
:
Update OptionsPerPos at the given position, setting the key n
to have the boolean value v.
Equations
- opts.setBool p n v = let e := Lean.KVMap.setBool (Lean.RBMap.findD opts p { entries := [] }) n v; Lean.RBMap.insert opts p e