inductive Aesop.TreeRef : Type

• goal (gref : GoalRef) : TreeRef
• rapp (rref : RappRef) : TreeRef
• mvarCluster (cref : MVarClusterRef) : TreeRef

@[specialize #[]]

partial def Aesop.traverseDown {m : Type → Type} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (visitGoalPre : GoalRef → m Bool) (visitGoalPost : GoalRef → m Unit) (visitRappPre : RappRef → m Bool) (visitRappPost : RappRef → m Unit) (visitMVarClusterPre : MVarClusterRef → m Bool) (visitMVarClusterPost : MVarClusterRef → m Unit) : TreeRef → m Unit

@[specialize #[]]

partial def Aesop.traverseUp {m : Type → Type} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (visitGoalPre : GoalRef → m Bool) (visitGoalPost : GoalRef → m Unit) (visitRappPre : RappRef → m Bool) (visitRappPost : RappRef → m Unit) (visitMVarClusterPre : MVarClusterRef → m Bool) (visitMVarClusterPost : MVarClusterRef → m Unit) : TreeRef → m Unit

@[inline]

def Aesop.preTraverseDown {m : Type → Type} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (visitGoal : GoalRef → m Bool) (visitRapp : RappRef → m Bool) (visitMVarCluster : MVarClusterRef → m Bool) : TreeRef → m Unit

Equations

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

@[inline]

def Aesop.preTraverseUp {m : Type → Type} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (visitGoal : GoalRef → m Bool) (visitRapp : RappRef → m Bool) (visitMVarCluster : MVarClusterRef → m Bool) : TreeRef → m Unit

Equations

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

@[inline]

def Aesop.postTraverseDown {m : Type → Type} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (visitGoal : GoalRef → m Unit) (visitRapp : RappRef → m Unit) (visitMVarCluster : MVarClusterRef → m Unit) : TreeRef → m Unit

Equations

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

@[inline]

def Aesop.postTraverseUp {m : Type → Type} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (visitGoal : GoalRef → m Unit) (visitRapp : RappRef → m Unit) (visitMVarCluster : MVarClusterRef → m Unit) : TreeRef → m Unit

Equations

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