rowToMessageData — Mathlib

Lean4
/-- Render a particular row of the Fitch table. -/
def rowToMessageData : List MessageData → List MessageData → List MessageData → List Entry → MetaM MessageData
  | line :: lines, dep :: deps, thm :: thms, en :: es => do
    let pipes := String.join (List.replicate en.depth "│ ")
    let pipes :=
      match en.status with
      | Status.sintro => s!"├ "
      | Status.intro => s! "│ {pipes}┌ "
      | Status.cintro => s! "│ {pipes}├ "
      | Status.lam => s! "│ {pipes}"
      | Status.reg => s! "│ {pipes}"
    let row := m! "{line }│{dep }│ {thm } {pipes }{en.type}\n"
    return (← rowToMessageData lines deps thms es).compose row
  | _, _, _, _ => return MessageData.nil
Похожие утверждения