Format Table

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

inductive Alignment : Type

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

• left : Alignment
• right : Alignment
• center : Alignment

@[implicit_reducible]

instance instInhabitedAlignment : Inhabited Alignment

def instInhabitedAlignment.default : Alignment

def instBEqAlignment.beq : Alignment → Alignment → Bool

@[implicit_reducible]

instance instBEqAlignment : BEq Alignment

def String.justify (s : String) (a : Alignment) (width : ℕ) : String

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

def formatTable (headers : Array String) (table : Array (Array String)) (alignments : Option (Array Alignment) := none) : String

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