Lean4
/-- Elaborates the terms like how `Lean.Elab.Tactic.addSimpTheorem` does,
abstracting their metavariables.
-/
def elabSubsingletonInsts (instTerms? : Option (Array Term)) : TermElabM (Array (Term × AbstractMVarsResult)) := do
if let some instTerms := instTerms? then
go instTerms.toList #[]
else
return #[]
where/-- Main loop for `addSubsingletonInsts`. -/
go (instTerms : List Term) (insts : Array (Term × AbstractMVarsResult)) :
TermElabM (Array (Term × AbstractMVarsResult)) := do
match instTerms with
| [] =>
return insts
| instTerm :: instTerms =>
let inst ←
withNewMCtxDepth <|
Term.withoutModifyingElabMetaStateWithInfo do
withRef instTerm <|
Term.withoutErrToSorry do
let e ← Term.elabTerm instTerm none
Term.synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true)
let e ← instantiateMVars e
unless (← isClass? (← inferType e)).isSome do
throwError "Not an instance. Term has type{indentD <| ← inferType e}"
if e.hasMVar then
let r ← abstractMVars e
let e' ←
forallBoundedTelescope (← inferType r.expr) r.numMVars fun args _ => do
let newBIs ←
args.filterMapM fun arg => do
if (← isClass? (← inferType arg)).isSome then
return some (arg.fvarId!, .instImplicit)
else
return none
withNewBinderInfos newBIs do
mkLambdaFVars args (r.expr.beta args)
pure { r with expr := e' }
else
pure { paramNames := #[], mvars := #[], expr := e }
go instTerms (insts.push (instTerm, inst))
