Status

Mathlib.Tactic.Explode.Datatypes

URI: https://scilib.ai/kg/mathlib#Mathlib.Explode.Status

Lean4

/-- How to display pipes (`│`) for this entry in the Fitch table . -/
inductive Status where/-- `├` Start intro (top-level) -/

  | sintro : Status/-- `Entry.depth` * `│` + `┌` Normal intro -/

  | intro : Status/-- `Entry.depth` * `│` + `├` Continuation intro -/

  | cintro : Status/-- `Entry.depth` * `│` -/

  | lam : Status/-- `Entry.depth` * `│` -/

  | reg : Status
  deriving Inhabited

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

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

Разделы

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

Аффилиация

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