nestedMap — Mathlib

Lean4
/-- `nestedMap f α (List (Array (List α)))` synthesizes the expression
`Functor.map (Functor.map (Functor.map f))`. `nestedMap` assumes that `α` appears in
`(List (Array (List α)))`.

(Similar to `nestedTraverse` but for `Functor`.) -/
partial def nestedMap (f v t : Expr) : TermElabM Expr := do
  let t ← instantiateMVars t
  if ← withNewMCtxDepth <| isDefEq t v then
    return f
  else if !v.occurs t.appFn! then
    let cl ← mkAppM ``Functor #[t.appFn!]
    let inst ← synthInstance cl
    let f' ← nestedMap f v t.appArg!
    mkAppOptM ``Functor.map #[t.appFn!, inst, none, none, f']
  else
    throwError "type {t } is not a functor with respect to variable {v}"
Похожие утверждения