Stained

Mathlib.Tactic.Linter.FlexibleLinter

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

Lean4

/-- `Stained` is the type of the stained locations: it can be
* a `Name` (typically of associated to the `FVarId` of a local declaration);
* the goal (`⊢`);
* the "wildcard" -- all the declaration in context (`*`).
-/
inductive Stained
  | name : Name → Stained
  | goal : Stained
  | wildcard : Stained
  deriving Repr, Inhabited, DecidableEq, Hashable

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

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

Разделы

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

Аффилиация

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