Lean4
/-- derive the `map` definition of a `Functor` -/
def mkMap (type : Name) (m : MVarId) : TermElabM Unit := do
let levels ← getLevelNames
let vars ← getFVarsNotImplementationDetails
let (#[α, β, f, x], m) ← m.introN 4 [`α, `β, `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)
mapConstructor ctor type (.fvar f) (.fvar α) (.fvar β) (vars.concat (.fvar β)) args₀ m.mvarId!
instantiateMVars m
m.assign e
