Mathlib.Lean.PrettyPrinter.Delaborator

Lean.PrettyPrinter.Delaborator.withBindingBodyUnusedName' definition

{α} (d : Syntax → Expr → DelabM α) : DelabM α

Full source

/-- 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 withBindingBodyUnusedName' {α} (d : Syntax → Expr → DelabM α) : DelabM α := do
  let n ← getUnusedName (← getExpr).bindingName! (← getExpr).bindingBody!
  withBindingBody' n (fun fvar => return (← mkAnnotatedIdent n fvar, fvar))
    (fun (stxN, fvar) => d stxN fvar)

Delaboration with fresh bound variable name

Informal description

Given a function `d` that takes a syntax tree node and an expression and returns a delaboration action, this definition processes the body of a lambda or pi expression by generating an unused name for the bound variable and then applying `d` to the annotated identifier and the fresh free variable. This allows for proper handling of bound variables in the delaboration process.

Lean.PrettyPrinter.Delaborator.OptionsPerPos.setBool definition

(opts : OptionsPerPos) (p : SubExpr.Pos) (n : Name) (v : Bool) : OptionsPerPos

Full source

/-- Update `OptionsPerPos` at the given position, setting the key `n`
to have the boolean value `v`. -/
def OptionsPerPos.setBool (opts : OptionsPerPos) (p : SubExpr.Pos) (n : Name) (v : Bool) :
    OptionsPerPos :=
  let e := opts.findD p {} |>.setBool n v
  opts.insert p e

Update boolean option at position in `OptionsPerPos`

Informal description

Given a position `p`, a name `n`, and a boolean value `v`, this function updates the `OptionsPerPos` structure by setting the value associated with the key `n` at position `p` to `v`. The function first retrieves the existing options at position `p` (or an empty set of options if none exist), updates the boolean value for the key `n`, and then inserts the updated options back into the `OptionsPerPos` structure at position `p`.

Lean.PrettyPrinter.Delaborator.annotateGoToDef definition

(stx : Term) (target : Name) : DelabM Term

Full source

/-- Annotates `stx` with the go-to-def information of `target`. -/
def annotateGoToDef (stx : Term) (target : Name) : DelabM Term := do
  let module := (← findModuleOf? target).getD (← getEnv).mainModule
  let some range ← findDeclarationRanges? target | return stx
  let stx ← annotateCurPos stx
  let location := { module, range := range.selectionRange }
  addDelabTermInfoaddDelabTermInfo (← getPos) stx (← getExpr) (location? := some location)
  return stx

Go-to-definition annotation for syntax terms

Informal description

The function `annotateGoToDef` takes a syntax term `stx` and a target name `target`, and annotates `stx` with the go-to-definition information for `target`. It retrieves the module and declaration range of `target`, annotates the current position in `stx`, and adds delaborator term information with the location of the target definition.

Lean.PrettyPrinter.Delaborator.annotateGoToSyntaxDef definition

(stx : Term) : DelabM Term

Full source

/-- Annotates `stx` with the go-to-def information of the notation used in `stx`. -/
def annotateGoToSyntaxDef (stx : Term) : DelabM Term := do
  annotateGoToDef stx stx.raw.getKind

Syntax go-to-definition annotation

Informal description

The function `annotateGoToSyntaxDef` takes a syntax term `stx` and annotates it with go-to-definition information for the kind of syntax used in `stx`. It uses the syntax kind (retrieved via `stx.raw.getKind`) as the target for the go-to-definition annotation.