instToMessageDataProjectionRule — Mathlib

Lean4

instance : ToMessageData ProjectionRule where
  toMessageData
    | .rename x₁ x₂ x₃ x₄ =>
      .group <|
        .nest 1 <|
          "rename ⟨" ++
              .joinSep [toMessageData x₁, toMessageData x₂, toMessageData x₃, toMessageData x₄] ("," ++ Format.line) ++
            "⟩"
    | .add x₁ x₂ =>
      .group <| .nest 1 <| "+⟨" ++ .joinSep [toMessageData x₁, toMessageData x₂] ("," ++ Format.line) ++ "⟩"
    | .erase x₁ x₂ =>
      .group <| .nest 1 <| "-⟨" ++ .joinSep [toMessageData x₁, toMessageData x₂] ("," ++ Format.line) ++ "⟩"
    | .prefix x₁ x₂ =>
      .group <| .nest 1 <| "prefix ⟨" ++ .joinSep [toMessageData x₁, toMessageData x₂] ("," ++ Format.line) ++ "⟩"

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