getFVarIdAt

Mathlib.Tactic.Core

URI: https://scilib.ai/kg/mathlib#Lean.Elab.Tactic.getFVarIdAt

Lean4

/-- Elaborate syntax for an `FVarId` in the local context of the given goal. -/
def getFVarIdAt (goal : MVarId) (id : Syntax) : TacticM FVarId :=
  withRef id
    (do
      -- use apply-like elaboration to suppress insertion of implicit arguments

      let e ←
        goal.withContext do
            elabTermForApply id (mayPostpone := false)
      match e with
      | Expr.fvar fvarId =>
        return fvarId
      | _ =>
        throwError "unexpected term '{e}'; expected single reference to variable")

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

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

Разделы

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

Аффилиация

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