The delaborator is the first stage of the pretty printer, and the inverse of the elaborator: it turns fully elaborated Expr core terms back into surface-level Syntax, omitting some implicit information again and using higher-level syntax abstractions like notations where possible. The exact behavior can be customized using pretty printer options; activating pp.all should guarantee that the delaborator is injective and that re-elaborating the resulting Syntax round-trips.

Pretty printer options can be given not only for the whole term, but also specific subterms. This is used both when automatically refining pp options until round-trip and when interactively selecting pp options for a subterm (both TBD). The association of options to subterms is done by assigning a unique, synthetic Nat position to each subterm derived from its position in the full term. This position is added to the corresponding Syntax object so that elaboration errors and interactions with the pretty printer output can be traced back to the subterm.

The delaborator is extensible via the [delab] attribute.

structure Lean.PrettyPrinter.Delaborator.Context : Type

• optionsPerPos : OptionsPerPos
• currNamespace : Name
• openDecls : List OpenDecl
• inPattern : Bool
• subExpr : SubExpr
• depth : Nat

  Current recursion depth during delaboration. Used by the pp.deepTerms false option.

structure Lean.PrettyPrinter.Delaborator.State : Type

• steps : Nat

  The number of delab steps so far. Used by pp.maxSteps to stop delaboration.

• infos : SubExpr.PosMap Elab.Info

  We attach Elab.Info at various locations in the Syntax output in order to convey its semantics. While the elaborator emits InfoTrees, here we have no real text location tree to traverse, so we use a flattened map.

• holeIter : SubExpr.HoleIterator

  See SubExpr.nextExtraPos.

opaque Lean.PrettyPrinter.Delaborator.delabFailureId : InternalExceptionId

@[reducible, inline]

abbrev Lean.PrettyPrinter.Delaborator.DelabM (α : Type) : Type

Equations

• Lean.PrettyPrinter.Delaborator.DelabM = ReaderT Lean.PrettyPrinter.Delaborator.Context (StateRefT' IO.RealWorld Lean.PrettyPrinter.Delaborator.State Lean.MetaM)

@[reducible, inline]

abbrev Lean.PrettyPrinter.Delaborator.Delab : Type

Equations

• Lean.PrettyPrinter.Delaborator.Delab = Lean.PrettyPrinter.Delaborator.DelabM Lean.Term

instance Lean.PrettyPrinter.Delaborator.instInhabitedDelabM {α : Type} : Inhabited (DelabM α)

Equations

• Lean.PrettyPrinter.Delaborator.instInhabitedDelabM = { default := throw default }

@[inline]

def Lean.PrettyPrinter.Delaborator.orElse {α : Type} (d₁ : DelabM α) (d₂ : Unit → DelabM α) : DelabM α

Equations

• Lean.PrettyPrinter.Delaborator.orElse d₁ d₂ = Lean.catchInternalId Lean.PrettyPrinter.Delaborator.delabFailureId d₁ fun (x : Lean.Exception) => d₂ ()

def Lean.PrettyPrinter.Delaborator.failure {α : Type} : DelabM α

Equations

• Lean.PrettyPrinter.Delaborator.failure = throw (Lean.Exception.internal Lean.PrettyPrinter.Delaborator.delabFailureId)

instance Lean.PrettyPrinter.Delaborator.instAlternativeDelabM : Alternative DelabM

Equations

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

instance Lean.PrettyPrinter.Delaborator.instOrElseDelabM {α : Type} : OrElse (DelabM α)

Equations

• Lean.PrettyPrinter.Delaborator.instOrElseDelabM = { orElse := Lean.PrettyPrinter.Delaborator.orElse }

@[instance 100]

instance Lean.PrettyPrinter.Delaborator.instMonadReaderOfSubExprDelabM : MonadReaderOf SubExpr DelabM

Equations

• Lean.PrettyPrinter.Delaborator.instMonadReaderOfSubExprDelabM = { read := Lean.PrettyPrinter.Delaborator.Context.subExpr <$> read }

@[instance 100]

instance Lean.PrettyPrinter.Delaborator.instMonadWithReaderOfSubExprDelabM : MonadWithReaderOf SubExpr DelabM

Equations

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

@[instance 100]

instance Lean.PrettyPrinter.Delaborator.instMonadStateOfHoleIteratorDelabM : MonadStateOf SubExpr.HoleIterator DelabM

Equations

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

instance Lean.PrettyPrinter.Delaborator.instMonadQuotationDelabM : MonadQuotation DelabM

Equations

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

opaque Lean.PrettyPrinter.Delaborator.delabAttribute : KeyedDeclsAttribute Delab

Registers a delaborator.

@[delab k] registers a declaration of type Lean.PrettyPrinter.Delaborator.Delab for the Lean.Expr constructor k. Multiple delaborators for a single constructor are tried in turn until the first success. If the term to be delaborated is an application of a constant c, elaborators for app.c are tried first; this is also done for Expr.consts ("nullary applications") to reduce special casing. If the term is an Expr.mdata with a single key k, mdata.k is tried first.

def Lean.PrettyPrinter.Delaborator.attrApp_delab_ : ParserDescr

@[app_delab c] registers a delaborator for applications with head constant c. Such delaborators also apply to the constant c itself (known as a "nullary application").

This attribute should be applied to definitions of type Lean.PrettyPrinter.Delaborator.Delab.

When defining delaborators for constant applications, one should prefer this attribute over @[delab app.c], as @[app_delab c] first performs name resolution on c in the current scope.

Equations

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

def Lean.PrettyPrinter.Delaborator.getExprKind : DelabM Name

Equations

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

def Lean.PrettyPrinter.Delaborator.getOptionsAtCurrPos : DelabM Options

Equations

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

def Lean.PrettyPrinter.Delaborator.getPPOption {α : Type} (opt : Options → α) : DelabM α

Evaluate option accessor, using subterm-specific options if set.

Equations

• Lean.PrettyPrinter.Delaborator.getPPOption opt = do let __do_lift ← Lean.PrettyPrinter.Delaborator.getOptionsAtCurrPos pure (opt __do_lift)

def Lean.PrettyPrinter.Delaborator.whenPPOption (opt : Options → Bool) (d : Delab) : Delab

Equations

• Lean.PrettyPrinter.Delaborator.whenPPOption opt d = do let b ← Lean.PrettyPrinter.Delaborator.getPPOption opt if b = true then d else failure

def Lean.PrettyPrinter.Delaborator.whenNotPPOption (opt : Options → Bool) (d : Delab) : Delab

Equations

• Lean.PrettyPrinter.Delaborator.whenNotPPOption opt d = do let b ← Lean.PrettyPrinter.Delaborator.getPPOption opt if b = true then failure else d

def Lean.PrettyPrinter.Delaborator.withOptionAtCurrPos {α : Type} (k : Name) (v : DataValue) (x : DelabM α) : DelabM α

Set the given option at the current position and execute x in this context.

Equations

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

def Lean.PrettyPrinter.Delaborator.annotatePos (pos : SubExpr.Pos) (stx : Term) : Term

Equations

• Lean.PrettyPrinter.Delaborator.annotatePos pos stx = { raw := Lean.Syntax.setInfo (Lean.SourceInfo.synthetic { byteIdx := pos } { byteIdx := pos }) stx.raw }

def Lean.PrettyPrinter.Delaborator.annotateCurPos (stx : Term) : Delab

Equations

• Lean.PrettyPrinter.Delaborator.annotateCurPos stx = do let __do_lift ← Lean.PrettyPrinter.Delaborator.SubExpr.getPos pure (Lean.PrettyPrinter.Delaborator.annotatePos __do_lift stx)

def Lean.PrettyPrinter.Delaborator.addTermInfo (pos : SubExpr.Pos) (stx : Syntax) (e : Expr) (isBinder : Bool := false) : DelabM Unit

Equations

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

def Lean.PrettyPrinter.Delaborator.addTermInfo.mkTermInfo (stx : Syntax) (e : Expr) (isBinder : Bool := false) : DelabM Elab.TermInfo

Equations

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

def Lean.PrettyPrinter.Delaborator.addFieldInfo (pos : SubExpr.Pos) (projName fieldName : Name) (stx : Syntax) (val : Expr) : DelabM Unit

Equations

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

def Lean.PrettyPrinter.Delaborator.addFieldInfo.mkFieldInfo (projName fieldName : Name) (stx : Syntax) (val : Expr) : DelabM Elab.FieldInfo

Equations

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

def Lean.PrettyPrinter.Delaborator.addDelabTermInfo (pos : SubExpr.Pos) (stx : Syntax) (e : Expr) (isBinder : Bool := false) (location? : Option DeclarationLocation := none) (docString? : Option String := none) (explicit : Bool := true) : DelabM Unit

Equations

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

def Lean.PrettyPrinter.Delaborator.annotateTermInfo (stx : Term) : Delab

Annotates the term with the current expression position and registers TermInfo to associate the term to the current expression.

Equations

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

def Lean.PrettyPrinter.Delaborator.annotateTermInfoUnlessAnnotated (stx : Term) : Delab

Annotates the term with the current expression position and registers TermInfo to associate the term to the current expression, unless the syntax has a synthetic position and associated Info already.

Equations

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

def Lean.PrettyPrinter.Delaborator.withAnnotateTermInfo (d : Delab) : Delab

Modifies the delaborator so that it annotates the resulting term using annotateTermInfo.

Equations

• Lean.PrettyPrinter.Delaborator.withAnnotateTermInfo d = do let stx ← d Lean.PrettyPrinter.Delaborator.annotateTermInfo stx

def Lean.PrettyPrinter.Delaborator.withAnnotateTermInfoUnlessAnnotated (d : Delab) : Delab

Modifies the delaborator so that it ensures resulting term is annotated using annotateTermInfoUnlessAnnotated.

Equations

• Lean.PrettyPrinter.Delaborator.withAnnotateTermInfoUnlessAnnotated d = do let stx ← d Lean.PrettyPrinter.Delaborator.annotateTermInfoUnlessAnnotated stx

def Lean.PrettyPrinter.Delaborator.getUnusedName (suggestion : Name) (body : Expr) (preserveName : Bool := false) : DelabM Name

Gets an name based on suggestion that is unused in the local context. Erases macro scopes. If pp.safeShadowing is true, then the name is allowed to shadow a name in the local context if the name does not appear in body.

If preserveName is false, then returns the name, possibly with fresh macro scopes added. If suggestion has macro scopes then the result does as well.

Equations

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

def Lean.PrettyPrinter.Delaborator.getUnusedName.bodyUsesSuggestion (body : Expr) (lctx : LocalContext) (suggestion' : Name) : Bool

Equations

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

def Lean.PrettyPrinter.Delaborator.mkAnnotatedIdent (n : Name) (e : Expr) : DelabM Ident

Creates an identifier that is annotated with the term e, using a fresh position using the HoleIterator.

Equations

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

def Lean.PrettyPrinter.Delaborator.withBindingBodyUnusedName {α : Type} (d : Syntax → DelabM α) (preserveName : Bool := false) : DelabM α

Enters the body of the current expression, which must be a lambda or forall. The binding variable is passed to d as Syntax, and it is an identifier that has been annotated with the fvar expression for the variable.

If preserveName is false (the default), gives the binder an unused name. Otherwise, it tries to preserve the textual form of the name, preserving whether it is hygienic.

Equations

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

inductive Lean.PrettyPrinter.Delaborator.OmissionReason : Type

• deep : OmissionReason
• proof : OmissionReason
• maxSteps : OmissionReason
• string (s : String) : OmissionReason

def Lean.PrettyPrinter.Delaborator.OmissionReason.toString : OmissionReason → String

Equations

• Lean.PrettyPrinter.Delaborator.OmissionReason.deep.toString = "Term omitted due to its depth (see option `pp.deepTerms`)."
• Lean.PrettyPrinter.Delaborator.OmissionReason.proof.toString = "Proof omitted (see option `pp.proofs`)."
• Lean.PrettyPrinter.Delaborator.OmissionReason.maxSteps.toString = "Term omitted due to reaching the maximum number of steps allowed for pretty printing this expression (see option `pp.maxSteps`)."
• (Lean.PrettyPrinter.Delaborator.OmissionReason.string s).toString = s

def Lean.PrettyPrinter.Delaborator.addOmissionInfo (pos : SubExpr.Pos) (stx : Syntax) (e : Expr) (reason : OmissionReason) : DelabM Unit

Equations

• Lean.PrettyPrinter.Delaborator.addOmissionInfo pos stx e reason = Lean.PrettyPrinter.Delaborator.addDelabTermInfo pos stx e false none (some reason.toString) false

def Lean.PrettyPrinter.Delaborator.withIncDepth {α : Type} (act : DelabM α) : DelabM α

Runs the delaborator act with increased depth. The depth is used when pp.deepTerms is false to determine what is a deep term. See also Lean.PrettyPrinter.Delaborator.Context.depth.

Equations

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

def Lean.PrettyPrinter.Delaborator.isShallowExpression (threshold : Nat) (e : Expr) : Bool

Returns true if e is a "shallow" expression. Local variables, constants, and other atomic expressions are always shallow. In general, an expression is considered to be shallow if its depth is at most threshold.

Since the implementation uses Lean.Expr.approxDepth, the threshold is clamped to [0, 254].

Equations

• Lean.PrettyPrinter.Delaborator.isShallowExpression threshold e = decide (e.approxDepth.toNat ≤ min 254 threshold)

def Lean.PrettyPrinter.Delaborator.shouldOmitExpr (e : Expr) : DelabM Bool

Returns true if, at the current depth, we should omit the term and use ⋯ rather than delaborating it. This function can only return true if pp.deepTerms is set to false. It also contains a heuristic to allow "shallow terms" to be delaborated, even if they appear deep in an expression, which prevents terms such as atomic expressions or OfNat.ofNat literals from being delaborated as ⋯.

Equations

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

def Lean.PrettyPrinter.Delaborator.shouldOmitProof (e : Expr) : DelabM Bool

Returns true if the given expression is a proof and should be omitted. This function only returns true if pp.proofs is set to false.

"Shallow" proofs are not omitted. The pp.proofs.threshold option controls the depth threshold for what constitutes a shallow proof. See Lean.PrettyPrinter.Delaborator.isShallowExpression.

Equations

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

def Lean.PrettyPrinter.Delaborator.omission (reason : OmissionReason) : Delab

Delaborates the current expression as ⋯ and attaches Elab.OmissionInfo, which influences how the subterm omitted by ⋯ is delaborated when hovered over.

Equations

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

partial def Lean.PrettyPrinter.Delaborator.delabFor : Name → Delab

partial def Lean.PrettyPrinter.Delaborator.delab : Delab

opaque Lean.PrettyPrinter.Delaborator.appUnexpanderAttribute : KeyedDeclsAttribute Unexpander

Registers an unexpander for applications of a given constant.

@[app_unexpander c] registers a Lean.PrettyPrinter.Unexpander for applications of the constant c. The unexpander is passed the result of pre-pretty printing the application without implicitly passed arguments. If pp.explicit is set to true or pp.notation is set to false, it will not be called at all.

Unexpanders work as an alternative for delaborators (@[app_delab]) that can be used without special imports. This however also makes them much less capable since they can only transform syntax and don't have access to the expression tree.

def Lean.PrettyPrinter.delabCore {α : Type} (e : Expr) (optionsPerPos : Delaborator.OptionsPerPos := ∅) (delab : Delaborator.DelabM α) : MetaM (α × SubExpr.PosMap Elab.Info)

Equations

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

def Lean.PrettyPrinter.delab (e : Expr) (optionsPerPos : Delaborator.OptionsPerPos := ∅) : MetaM Term

"Delaborate" the given term into surface-level syntax using the default and given subterm-specific options.

Equations

• Lean.PrettyPrinter.delab e optionsPerPos = do let __discr ← Lean.PrettyPrinter.delabCore e optionsPerPos Lean.PrettyPrinter.Delaborator.delab match __discr with | (stx, snd) => pure stx