Lean4
/-- Run the `useLoop` on the main goal then discharge remaining explicit `Prop` arguments. -/
def runUse (eager : Bool) (discharger : TacticM Unit) (args : List Term) : TacticM Unit := do
let egoals ←
focus do
let (egoals, acc, insts) ←
useLoop eager (← getGoals) args []
[]
-- Try synthesizing instance arguments
for inst in insts do
if !(← inst.isAssigned) then
discard <|
inst.withContext <|
observing? do
inst.assign
(← synthInstance (← inst.getType))
-- Set the goals.
setGoals (egoals ++ acc)
pruneSolvedGoals
pure egoals
for g in egoals do
if !(← g.isAssigned) then
g.withContext
(do
if ← isProp (← g.getType) then
trace[tactic.use]"running discharger on {g}"
discard <| run g discharger)
