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.
- optionsPerPos : Lean.PrettyPrinter.Delaborator.OptionsPerPos
- currNamespace : Lake.Name
- openDecls : List Lean.OpenDecl
- inPattern : Bool
- subExpr : Lean.SubExpr
Instances For
- infos : Lean.SubExpr.PosMap Lean.Elab.Info
We attach
Elab.Info
at various locations in theSyntax
output in order to convey its semantics. While the elaborator emitsInfoTree
s, here we have no real text location tree to traverse, so we use a flattened map. See
SubExpr.nextExtraPos
.
Instances For
Instances For
Instances For
Instances For
Instances For
Evaluate option accessor, using subterm-specific options if set.
Instances For
Instances For
Instances For
Set the given option at the current position and execute x
in this context.
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
"Delaborate" the given term into surface-level syntax using the default and given subterm-specific options.