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"]

Equations

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

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

Render a particular row of the Fitch table.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Explode.rowToMessageData x✝² x✝¹ x✝ x = pure Lean.MessageData.nil

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

Given all Entries, return the entire Fitch table.

Equations

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