Lean4
/-- derive the `traverse` definition of a `Traversable` instance -/
def mkTraverse (type : Name) (m : MVarId) : TermElabM Unit := do
let vars ← getFVarsNotImplementationDetails
let levels ← getLevelNames
let (#[_, applInst, α, β, f, x], m) ← m.introN 6 [`m, `applInst, `α, `β, `f, `x] |
failure
m.withContext do
let xtype ← x.getType
let target ← m.getType >>= instantiateMVars
let motive ← mkLambdaFVars #[.fvar x] target
let e ←
mkCasesOnMatch type (levels.map Level.param) (vars.concat (.fvar α)) motive [] (.fvar x) fun ctor fields => do
let m ← mkFreshExprSyntheticOpaqueMVar target
let args := fields.map Expr.fvar
let args₀ ←
args.mapM fun a => do
let b := xtype.occurs (← inferType a)
return (b, a)
traverseConstructor ctor type (.fvar applInst) (.fvar f) (.fvar α) (.fvar β) (vars.concat (.fvar β)) args₀
m.mvarId!
instantiateMVars m
m.assign e
