Documentation

Init.Data.Format.Basic

Determines how groups should have linebreaks inserted when the text would overfill its remaining space.

Instances For
    inductive Std.Format :

    A string with pretty-printing information for rendering in a column-width-aware way.

    The pretty-printing algorithm is based on Wadler's paper A Prettier Printer.

    Instances For
      Equations
      Instances For
        Equations
        Instances For
          Equations

          A monad in which we can pretty-print Format objects.

          • pushOutput : Stringm Unit
          • pushNewline : Natm Unit
          • currColumn : m Nat
          • startTag : Natm Unit

            Start a scope tagged with n.

          • endTags : Natm Unit

            Exit the scope of n-many opened tags.

          Instances
            def Std.Format.prettyM {m : TypeType} (f : Lean.Format) (w : Nat) (indent : optParam Nat 0) [Monad m] [Std.Format.MonadPrettyFormat m] :

            Render the given f : Format with a line width of w. indent is the starting amount to indent each line by.

            Equations
            Instances For
              @[inline]

              Create a format l ++ f ++ r with a flatten group. FlattenBehaviour is allOrNone; for fill use bracketFill.

              Equations
              Instances For
                @[inline]

                Creates the format "(" ++ f ++ ")" with a flattening group.

                Equations
                Instances For
                  @[inline]

                  Creates the format "[" ++ f ++ "]" with a flattening group.

                  Equations
                  Instances For
                    @[inline]

                    Same as bracket except uses the fill flattening behaviour.

                    Equations
                    Instances For

                      Default indentation.

                      Equations
                      Instances For

                        Default width of the targeted output pane.

                        Equations
                        Instances For

                          Nest with the default indentation amount.

                          Equations
                          Instances For

                            Insert a newline and then f, all nested by the default indent amount.

                            Equations
                            Instances For
                              Equations
                              • One or more equations did not get rendered due to their size.
                              @[export lean_format_pretty]

                              Pretty-print a Format object as a string with expected width w.

                              Equations
                              Instances For
                                class Std.ToFormat (α : Type u) :

                                Class for converting a given type α to a Format object for pretty-printing. See also Repr, which also outputs a Format object.

                                Instances

                                  Intersperse the given list (each item printed with format) with the given sep format.

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

                                    Format each item in items and prepend prefix pre.

                                    Equations
                                    Instances For

                                      Format each item in items and append suffix.

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