Additions to the delaborator #
def
Lean.PrettyPrinter.Delaborator.SubExpr.withBindingBody'
{α : Type}
{m : Type → Type}
[Monad m]
[MonadReaderOf Lean.SubExpr m]
[MonadWithReaderOf Lean.SubExpr m]
[MonadControlT Lean.MetaM m]
(n : Lean.Name)
(x : Lean.Expr → m α)
:
m α
Assuming the current expression is a lambda or pi,
descend into the body using the given name n for the username of the fvar.
Provides x with the fresh fvar for the bound variable.
See also Lean.PrettyPrinter.Delaborator.SubExpr.withBindingBody.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
- Lean.PrettyPrinter.Delaborator.OptionsPerPos.setBool opts p n v = let e := Lean.KVMap.setBool (Lean.RBMap.findD opts p { entries := [] }) n v; Lean.RBMap.insert opts p e