Documentation

Aesop.Tree.ExtractProof

source
def Aesop.Goal.extractProof (root : Goal) :
Lean.MetaM Unit
Equations
    Instances For
      source
      def Aesop.extractProof :
      TreeM Unit
      Equations
        Instances For
          source
          def Aesop.Goal.extractSafePrefix (root : Goal) :
          Lean.MetaM (Array Lean.MVarId)
          Equations
            Instances For
              source
              def Aesop.extractSafePrefix :
              TreeM (Array Lean.MVarId)
              Equations
                Instances For