Lean4
/-- derive the `traverse` definition and declare `Traversable` using this. -/
def deriveTraversable (m : MVarId) : TermElabM Unit := do
let docCtx := (← getLCtx, ← getLocalInstances)
let levels ← getLevelNames
let vars ← getFVarsNotImplementationDetails
let .app (.const ``Traversable _) F ← m.getType >>= instantiateMVars |
failure
let some n := F.getAppFn.constName? |
failure
let d ← getConstInfo n
let [m] ← run m <| evalTactic (← `(tactic| refine { traverse := @(?_) })) |
failure
let t ← m.getType >>= instantiateMVars
let n' := .mkStr n "traverse"
withDeclName n' <|
withAuxDecl (.mkSimple "traverse") t n' fun ad => do
let m' := (← mkFreshExprSyntheticOpaqueMVar t).mvarId!
mkTraverse n m'
let e ← instantiateMVars (mkMVar m')
let e := e.replaceFVar ad (mkAppN (.const n' (levels.map Level.param)) vars.toArray)
let e' ← mkLambdaFVars vars.toArray e
let t' ← mkForallFVars vars.toArray t
addPreDefinitions docCtx
#[{ ref := .missing
kind := .def
levelParams := levels
binders := mkNullNode #[]
modifiers :=
{ isUnsafe := d.isUnsafe
isProtected := true }
declName := n'
type := t'
value := e'
termination := .none }] { }
m.assign (mkAppN (mkConst n' (levels.map Level.param)) vars.toArray)
