instToStringStained

Mathlib.Tactic.Linter.FlexibleLinter

URI: https://scilib.ai/kg/mathlib#Mathlib.Linter.Flexible.instToStringStained

Lean4

/-- Converting a `Stained` to a `String`:
* a `Name` is represented by the corresponding string;
* `goal` is represented by `⊢`;
* `wildcard` is represented by `*`.
-/
instance : ToString Stained where
  toString
    | .name n => n.toString
    | .goal => "⊢"
    | .wildcard => "*"

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

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

Разделы

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

Аффилиация

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