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

• One or more equations did not get rendered due to their size.

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.

Equations

• opts.setBool p n v = Lean.RBMap.insert opts p (Lean.KVMap.setBool (Lean.RBMap.findD opts p { }) n v)

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• Lean.PrettyPrinter.Delaborator.annotateGoToSyntaxDef stx = Lean.PrettyPrinter.Delaborator.annotateGoToDef stx stx.raw.getKind