structure Aesop.GoalWithMVars : Type

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

def Aesop.instInhabitedGoalWithMVars.default : GoalWithMVars

Equations

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

@[implicit_reducible]

instance Aesop.instInhabitedGoalWithMVars : Inhabited GoalWithMVars

Equations

• Aesop.instInhabitedGoalWithMVars = { default := Aesop.instInhabitedGoalWithMVars.default }

@[implicit_reducible]

instance Aesop.instReprGoalWithMVars : Repr GoalWithMVars

Equations

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

@[implicit_reducible]

instance Aesop.instBEqGoalWithMVars : BEq GoalWithMVars

Equations

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

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

Equations

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