rootExpr

Mathlib.Lean.GoalsLocation

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

Lean4

/-- The root expression of the position specified by the `GoalsLocation`. -/
def rootExpr : GoalsLocation → MetaM Expr
  | ⟨_, .hyp fvarId⟩ => do
    instantiateMVars (← fvarId.getType)
  | ⟨_, .hypType fvarId _⟩ => do
    instantiateMVars (← fvarId.getType)
  | ⟨_, .hypValue fvarId _⟩ => do
    instantiateMVars (← fvarId.getDecl).value
  | ⟨mvarId, .target _⟩ => do
    instantiateMVars (← mvarId.getType)

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

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

Разделы

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

Аффилиация

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