Documentation

Aesop.Script.GoalWithMVars

source
structure Aesop.GoalWithMVars :
Type
Instances For
    source
    @[instance_reducible]
    instance Aesop.instInhabitedGoalWithMVars :
    Inhabited GoalWithMVars
    source
    @[instance_reducible]
    instance Aesop.instReprGoalWithMVars :
    Repr GoalWithMVars
    source
    @[instance_reducible]
    instance Aesop.instBEqGoalWithMVars :
    BEq GoalWithMVars
    source
    def Aesop.GoalWithMVars.ofMVarId (goal : Lean.MVarId) :
    Lean.MetaM GoalWithMVars
    Instances For