instToMessageDataParsedProjectionData

Mathlib.Tactic.Simps.Basic

URI: https://scilib.ai/kg/mathlib#Simps.instToMessageDataParsedProjectionData

Lean4

instance : ToMessageData ParsedProjectionData where
  toMessageData
    | ⟨x₁, x₂, x₃, x₄, x₅, x₆, x₇, x₈, x₉⟩ =>
      .group <|
        .nest 1 <|
          "⟨" ++
              .joinSep
                [toMessageData x₁, toMessageData x₂, toMessageData x₃, toMessageData x₄, toMessageData x₅,
                  toMessageData x₆, toMessageData x₇, toMessageData x₈, toMessageData x₉]
                ("," ++ Format.line) ++
            "⟩"

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

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

Разделы

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

Аффилиация

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