Lean4
/-- Turn tactic syntax into a discharger function. -/
def tacticToDischarge (tacticCode : TSyntax `tactic) : Expr → MetaM (Option Expr) := fun e =>
withTraceNode `Meta.Tactic.fun_prop
(fun r => do
pure s! "[{ExceptToEmoji.toEmoji r}] discharging: {← ppExpr e}")
(do
let mvar ← mkFreshExprSyntheticOpaqueMVar e `funProp.discharger
let runTac? : TermElabM (Option Expr) :=
try
withoutModifyingStateWithInfoAndMessages
(do
instantiateMVarDeclMVars mvar.mvarId!
let _ ←
withSynthesize (postpone := .no) do
Tactic.run mvar.mvarId! (Tactic.evalTactic tacticCode *> Tactic.pruneSolvedGoals)
let result ← instantiateMVars mvar
if result.hasExprMVar then
return none
else
return some result)
catch _ =>
return none
let (result?, _) ← runTac?.run { } { }
return result?)
