pos

Mathlib.Lean.GoalsLocation

URI: https://scilib.ai/kg/mathlib#Lean.SubExpr.GoalsLocation.pos

Lean4

/-- The `SubExpr.Pos` specified by the `GoalsLocation`. -/
def pos : GoalsLocation → Pos
  | ⟨_, .hyp _⟩ => .root
  | ⟨_, .hypType _ pos⟩ => pos
  | ⟨_, .hypValue _ pos⟩ => pos
  | ⟨_, .target pos⟩ => pos

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

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

Разделы

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

Аффилиация

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