getHypothesisRewrites

Mathlib.Tactic.Widget.LibraryRewrite

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.LibraryRewrite.getHypothesisRewrites

Lean4

/-- Return all applicable hypothesis rewrites of `e`. Similar to `getImportRewrites`. -/
def getHypothesisRewrites (e : Expr) (except : Option FVarId) : MetaM (Array (Array (Rewrite × FVarId))) := do
  let (candidates, _) ← (← getHypotheses except).getMatch e (unify := false) (matchRootStar := true)
  let candidates := (← MonadExcept.ofExcept candidates).flatten
  candidates.mapM <|
      Array.filterMapM fun (fvarId, symm) =>
        tryCatchRuntimeEx
          (do
            Option.map (·, fvarId) <$> checkRewrite (.fvar fvarId) e symm)
          fun _ => return none

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

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

Разделы

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

Аффилиация

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