Documentation

Lean.PrettyPrinter.Delaborator.Basic

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.

Instances For
    • steps : Nat

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

    • 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.

    • See SubExpr.nextExtraPos.

    Instances For
      @[reducible, inline]
      Equations
        Instances For
          @[reducible, inline]
          Equations
            Instances For
              @[inline]
              def Lean.PrettyPrinter.Delaborator.orElse {α : Type} (d₁ : DelabM α) (d₂ : UnitDelabM α) :
              Equations
                Instances For
                  Equations
                    Instances For

                      @[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
                        Instances For

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

                          Equations
                            Instances For
                              Equations
                                Instances For
                                  Equations
                                    Instances For

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

                                      Equations
                                        Instances For
                                          Equations
                                            Instances For
                                              Equations
                                                Instances For
                                                  def Lean.PrettyPrinter.Delaborator.addFieldInfo (pos : SubExpr.Pos) (projName fieldName : Name) (stx : Syntax) (val : Expr) :
                                                  Equations
                                                    Instances For
                                                      Equations
                                                        Instances For
                                                          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) :
                                                          Equations
                                                            Instances For

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

                                                              Equations
                                                                Instances For

                                                                  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
                                                                    Instances For

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

                                                                      Equations
                                                                        Instances For

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

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

                                                                              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
                                                                                Instances For
                                                                                  Equations
                                                                                    Instances For

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

                                                                                      Equations
                                                                                        Instances For

                                                                                          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
                                                                                            Instances For
                                                                                              Equations
                                                                                                Instances For

                                                                                                  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
                                                                                                    Instances For

                                                                                                      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
                                                                                                        Instances For

                                                                                                          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
                                                                                                            Instances For

                                                                                                              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
                                                                                                                Instances For

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

                                                                                                                  Equations
                                                                                                                    Instances For
                                                                                                                      Equations
                                                                                                                        Instances For

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

                                                                                                                          Equations
                                                                                                                            Instances For