structure Aesop.GoalWithMVars : Type

• goal : Lean.MVarId
• mvars : Lean.HashSet Lean.MVarId

instance Aesop.instInhabitedGoalWithMVars : Inhabited Aesop.GoalWithMVars

Equations

• Aesop.instInhabitedGoalWithMVars = { default := { goal := default, mvars := default } }

instance Aesop.instReprGoalWithMVars : Repr Aesop.GoalWithMVars

Equations

• One or more equations did not get rendered due to their size.

instance Aesop.instBEqGoalWithMVars : BEq Aesop.GoalWithMVars

Equations

• Aesop.instBEqGoalWithMVars = { beq := fun (g₁ g₂ : Aesop.GoalWithMVars) => g₁.goal == g₂.goal }

def Aesop.GoalWithMVars.ofMVarId (goal : Lean.MVarId) : Lean.MetaM Aesop.GoalWithMVars

Equations

• Aesop.GoalWithMVars.ofMVarId goal = do let __do_lift ← goal.getMVarDependencies pure { goal := goal, mvars := __do_lift }