mapField

Mathlib.Tactic.DeriveTraversable

URI: https://scilib.ai/kg/mathlib#Mathlib.Deriving.Traversable.mapField

Lean4

/-- similar to `traverseField` but for `Functor` -/
def mapField (n : Name) (cl f α β e : Expr) : TermElabM Expr := do
  let t ← whnf (← inferType e)
  if t.getAppFn.constName = some n then
    throwError"recursive types not supported"
  else if α.eqv e then
    return β
  else if α.occurs t then
    let f' ← nestedMap f α t
    return f'.app e
  else if
    ←
      (match t with
      | .app t' _ => withNewMCtxDepth <| isDefEq t' cl
      | _ => return false) then
    mkAppM ``Comp.mk #[e]
  else
    return e

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

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

Разделы

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

Аффилиация

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