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

Equations

• root.extractProof = 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 __do_lift.extractProof

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 __do_lift.extractSafePrefix