← Mathematical handbook

def Aesop.GoalRef.free (gref : GoalRef) : BaseIO Unit

Equations

• gref.free = do let __x ← Aesop.mkDummyRefs✝ match __x with | (dgref, dcref) => Aesop.freeGoalRef✝ dgref dcref gref

def Aesop.RappRef.free (rref : RappRef) : BaseIO Unit

Equations

• rref.free = do let __x ← Aesop.mkDummyRefs✝ match __x with | (dgref, dcref) => Aesop.freeRappRef✝ dgref dcref rref

def Aesop.MVarClusterRef.free (cref : MVarClusterRef) : BaseIO Unit

Equations

• cref.free = do let __x ← Aesop.mkDummyRefs✝ match __x with | (dgref, dcref) => Aesop.freeMVarClusterRef✝ dgref dcref cref

def Aesop.freeTree : TreeM Unit

Equations

• Aesop.freeTree = do let __do_lift ← getThe Aesop.Tree liftM __do_lift.root.free