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

instance instInhabitedAlignment : Inhabited Alignment

Equations

• instInhabitedAlignment = { default := Alignment.left }

instance instBEqAlignment : BEq Alignment

Equations

• instBEqAlignment = { beq := beqAlignment✝ }

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

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

Equations

• s.justify Alignment.left width = String.rightpad width ' ' s
• s.justify Alignment.right width = String.leftpad width ' ' s
• s.justify Alignment.center width = String.replicate ((width - s.length) / 2) ' ' ++ s ++ String.replicate (width - s.length - (width - s.length) / 2) ' '

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

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.