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
      Equations
      • pushOutput : Stringm Unit
      • pushNewline : Natm Unit
      • currColumn : m Nat
      • Start a scope tagged with n.

        startTag : Natm Unit
      • Exit the scope of n-many opened tags.

        endTags : Natm Unit

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

      Instances
        def Std.Format.prettyM {m : TypeType} (f : Lean.Format) (w : Nat) (indent : optParam Nat 0) [inst : Monad m] [inst : 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
        @[inline]

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

        Equations
        @[inline]

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

        Equations
        @[inline]

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

        Equations
        @[inline]

        Same as bracket except uses the fill flattening behaviour.

        Equations

        Default indentation.

        Equations

        Default width of the targeted output pane.

        Equations

        Nest with the default indentation amount.

        Equations

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

        Equations
        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
        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
          def Std.Format.joinSep {α : Type u} [inst : Lean.ToFormat α] :

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

          Equations
          def Std.Format.prefixJoin {α : Type u} [inst : Lean.ToFormat α] (pre : Lean.Format) :

          Format each item in items and prepend prefix pre.

          Equations

          Format each item in items and append suffix.

          Equations