Documentation

Mathlib.Util.FormatTable

Format Table #

This file provides a simple function for formatting a two-dimensional array of Strings into a markdown-compliant table.

inductive Alignment :

Possible alignment modes for each table item: left-aligned, right-aligned and centered.

Instances For
    def String.justify (s : String) (a : Alignment) (width : Nat) :

    Align a String s to the left, right, or center within a field of width width.

    Equations
    Instances For
      def formatTable (headers : Array String) (table : Array (Array String)) (alignments : optParam (Option (Array Alignment)) none) :

      Render a two-dimensional array of Stringsinto a markdown-compliant table. `headersis a list of column headers, `tableis a 2D array of cell contents, `alignments` describes how to align each table column (default: left-aligned)

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