entriesToMessageData

Mathlib.Tactic.Explode.Pretty

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

Lean4

/-- Given all `Entries`, return the entire Fitch table. -/
def entriesToMessageData (entries : Entries) : MetaM MessageData := do
  -- ['1', '2', '3']

  let paddedLines ← padRight <| entries.l.map fun entry => m! "{entry.line!}"
  let paddedDeps ←
    padRight <|
        entries.l.map fun entry =>
          String.intercalate "," <|
            entry.deps.map
              (fun dep => (dep.map toString).getD "_")
                -- ['p  ', 'hP ', '∀I ']

  let paddedThms ← padRight <| entries.l.map (·.thm)
  rowToMessageData paddedLines paddedDeps paddedThms entries.l

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

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

Разделы

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

Аффилиация

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