traverseField — Mathlib

Lean4
/-- For a sum type `inductive Foo (α : Type) | foo1 : List α → ℕ → Foo α | ...`
``traverseField `Foo f `α `(x : List α)`` synthesizes
`traverse f x` as part of traversing `foo1`. -/
def traverseField (n : Name) (cl f v e : Expr) : TermElabM (Bool × Expr) := do
  let t ← whnf (← inferType e)
  if t.getAppFn.constName = some n then
    throwError"recursive types not supported"
  else if v.occurs t then
    let f' ← nestedTraverse f v t
    return (true, f'.app e)
  else if
    ←
      (match t with
      | .app t' _ => withNewMCtxDepth <| isDefEq t' cl
      | _ => return false) then
    Prod.mk true <$> mkAppM ``Comp.mk #[e]
  else
    return (false, e)
Похожие утверждения