padRight

Mathlib.Tactic.Explode.Pretty

URI: https://scilib.ai/kg/mathlib#Mathlib.Explode.padRight

Lean4

/-- Given a list of `MessageData`s, make them of equal length.
We need this in order to form columns in our Fitch table.

```lean
padRight ["hi", "hello"] = ["hi   ", "hello"]
```
-/
def padRight (mds : List MessageData) : MetaM (List MessageData) := do
  -- 1. Find the max length of the word in a list

  let mut maxLength := 0
  for md in mds do
    maxLength := max maxLength (← md.toString).length
  let pad (md : MessageData) : MetaM MessageData := do
    let padWidth : Nat := maxLength - (← md.toString).length
    return md ++ "".pushn ' ' padWidth
  mds.mapM pad

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru