reassocExpr'

Mathlib.Tactic.CategoryTheory.Reassoc

URI: https://scilib.ai/kg/mathlib#CategoryTheory.reassocExpr'

Lean4

/-- Version of `reassocExpr` for the `TermElabM` monad. Handles instance metavariables automatically.
-/
def reassocExpr' (pf : Expr) (type? : Option Expr) : TermElabM Expr := do
  let (e, insts) ← reassocExpr pf type?
  for inst in insts do
    inst.withContext do
        unless ← Term.synthesizeInstMVarCore inst do
          Term.registerSyntheticMVarWithCurrRef inst (.typeClass none)
  return e

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

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

Разделы

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

Аффилиация

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