propagateInstImplicit

Mathlib.Tactic.CC.Addition

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.CC.CCM.propagateInstImplicit

Lean4

/-- Record the instance `e` and add it to the set of known defeq instances. -/
def propagateInstImplicit (e : Expr) : CCM Unit := do
  let type ← inferType e
  let type ← normalize type
  match (← get).instImplicitReprs[type]? with
  | some l =>
    for e' in l do
      if ← pureIsDefEq e e' then
        pushReflEq e e'
        return
    modify fun ccs => { ccs with instImplicitReprs := ccs.instImplicitReprs.insert type (e :: l) }
  | none =>
    modify fun ccs => { ccs with instImplicitReprs := ccs.instImplicitReprs.insert type [e] }

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

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

Разделы

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

Аффилиация

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