def Aesop.Goal.extractProof (root : Goal) : Lean.MetaM Unit

Equations

• root.extractProof = do let __do_lift ← Lean.getEnv Aesop.extractProofGoal✝ __do_lift root

def Aesop.extractProof : TreeM Unit

Equations

• Aesop.extractProof = do let __do_lift ← Aesop.getRootGoal let __do_lift ← ST.Ref.get __do_lift liftM __do_lift.extractProof

def Aesop.Goal.extractSafePrefix (root : Goal) : Lean.MetaM (Array Lean.MVarId)

Equations

• root.extractSafePrefix = do let __do_lift ← Lean.getEnv let __discr ← StateRefT'.run (Aesop.extractSafePrefixGoal✝ __do_lift root) { } match __discr with | (fst, state) => pure state.goals

def Aesop.extractSafePrefix : TreeM (Array Lean.MVarId)

Equations

• Aesop.extractSafePrefix = do let __do_lift ← Aesop.getRootGoal let __do_lift ← ST.Ref.get __do_lift liftM __do_lift.extractSafePrefix