toMessageData

Mathlib.Tactic.Widget.LibraryRewrite

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.LibraryRewrite.Rewrite.toMessageData

Lean4

/-- Represent a `Rewrite` as `MessageData`. -/
def toMessageData (rw : Rewrite) (name : Name) : MetaM MessageData := do
  let extraGoals ←
    rw.extraGoals.filterMapM fun (mvarId, bi) => do
        if bi.isExplicit then
          return some m!"⊢ {← mvarId.getType}"
        return none
  let list := [m! "{rw.replacement}"] ++ extraGoals.toList ++ [m! "{name}"]
  return .group <| .nest 2 <| "· " ++ .joinSep list "\n"

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

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

Разделы

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

Аффилиация

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