nestedTraverse — Mathlib

Lean4
/-- `nestedTraverse f α (List (Array (List α)))` synthesizes the expression
`traverse (traverse (traverse f))`. `nestedTraverse` assumes that `α` appears in
`(List (Array (List α)))` -/
partial def nestedTraverse (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 ``Traversable #[t.appFn!]
    let inst ← synthInstance cl
    let f' ← nestedTraverse f v t.appArg!
    mkAppOptM ``Traversable.traverse #[t.appFn!, inst, none, none, none, none, f']
  else
    throwError "type {t } is not traversable with respect to variable {v}"
Похожие утверждения