Documentation

Aesop.Script.GoalWithMVars

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