initialPropToFVar

Mathlib.Tactic.GeneralizeProofs

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.GeneralizeProofs.initialPropToFVar

Lean4

/-- Create a mapping of all propositions in the local context to their fvars.
-/
def initialPropToFVar : MetaM (ExprMap Expr) := do
  -- Visit decls in reverse order so that in case there are duplicates,
    -- earlier proofs are preferred

  (← getLCtx).foldrM (init := { }) fun decl m => do
      if !decl.isImplementationDetail then
        let ty := (← instantiateMVars decl.type).cleanupAnnotations
        if ← Meta.isProp ty then
          return m.insert ty decl.toExpr
      return m

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

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

Разделы

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

Аффилиация

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