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.

def Lean.PrettyPrinter.Delaborator.OptionsPerPos.setBool (opts : OptionsPerPos) (p : SubExpr.Pos) (n : Name) (v : Bool) : OptionsPerPos

Update OptionsPerPos at the given position, setting the key n to have the Boolean value v.

def Lean.PrettyPrinter.Delaborator.annotateGoToDef (stx : Term) (target : Name) : DelabM Term

Annotates stx with the go-to-def information of target.

def Lean.PrettyPrinter.Delaborator.annotateGoToSyntaxDef (stx : Term) : DelabM Term

Annotates stx with the go-to-def information of the notation used in stx.