Documentation

Aesop.Script.GoalWithMVars

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