Explode command: pretty

This file contains UI code to render the Fitch table.

def Mathlib.Explode.padRight (mds : List Lean.MessageData) : Lean.MetaM (List Lean.MessageData)

Given a list of MessageDatas, make them of equal length. We need this in order to form columns in our Fitch table.

padRight ["hi", "hello"] = ["hi   ", "hello"]

def Mathlib.Explode.rowToMessageData : List Lean.MessageData → List Lean.MessageData → List Lean.MessageData → List Entry → Lean.MetaM Lean.MessageData

Render a particular row of the Fitch table.

def Mathlib.Explode.entriesToMessageData (entries : Entries) : Lean.MetaM Lean.MessageData

Given all Entries, return the entire Fitch table.