Additions to the delaborator #
def
Lean.PrettyPrinter.Delaborator.withBindingBodyUnusedName'
{α : Type}
(d : Syntax → Expr → DelabM α)
:
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
Instances For
def
Lean.PrettyPrinter.Delaborator.OptionsPerPos.setBool
(opts : OptionsPerPos)
(p : SubExpr.Pos)
(n : Name)
(v : Bool)
:
Update OptionsPerPos
at the given position, setting the key n
to have the boolean value v
.
Equations
Instances For
Annotates stx
with the go-to-def information of the notation used in stx
.