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
    Instances For
      Equations
      • Lean.PrettyPrinter.Delaborator.instInhabitedDelabM = { default := throw default }
      Equations
      Equations
      • Lean.PrettyPrinter.Delaborator.instOrElseDelabM = { orElse := Lean.PrettyPrinter.Delaborator.orElse }
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

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

            Equations
            Instances For

              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.
              Instances For
                Equations
                Instances For
                  Equations
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For

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

                                      Equations
                                      Instances For