fvarId?

Mathlib.Lean.GoalsLocation

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

Lean4

/-- The hypothesis specified by the `GoalsLocation`. -/
def fvarId? : GoalsLocation → Option FVarId
  | ⟨_, .hyp fvarId⟩ => fvarId
  | ⟨_, .hypType fvarId _⟩ => fvarId
  | ⟨_, .hypValue fvarId _⟩ => fvarId
  | ⟨_, .target _⟩ => none

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

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

Разделы

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

Аффилиация

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