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

Equations

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

def Aesop.extractProof : Aesop.TreeM Unit

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

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