- goal: Aesop.GoalRef → Aesop.TreeRef
- rapp: Aesop.RappRef → Aesop.TreeRef
- mvarCluster: Aesop.MVarClusterRef → Aesop.TreeRef
@[specialize #[]]
partial def
Aesop.traverseDown
{m : Type → Type}
[Monad m]
[MonadLiftT (ST IO.RealWorld) m]
(visitGoalPre : Aesop.GoalRef → m Bool)
(visitGoalPost : Aesop.GoalRef → m Unit)
(visitRappPre : Aesop.RappRef → m Bool)
(visitRappPost : Aesop.RappRef → m Unit)
(visitMVarClusterPre : Aesop.MVarClusterRef → m Bool)
(visitMVarClusterPost : Aesop.MVarClusterRef → m Unit)
:
Aesop.TreeRef → m Unit
@[specialize #[]]
partial def
Aesop.traverseUp
{m : Type → Type}
[Monad m]
[MonadLiftT (ST IO.RealWorld) m]
(visitGoalPre : Aesop.GoalRef → m Bool)
(visitGoalPost : Aesop.GoalRef → m Unit)
(visitRappPre : Aesop.RappRef → m Bool)
(visitRappPost : Aesop.RappRef → m Unit)
(visitMVarClusterPre : Aesop.MVarClusterRef → m Bool)
(visitMVarClusterPost : Aesop.MVarClusterRef → m Unit)
:
Aesop.TreeRef → m Unit
@[inline]
def
Aesop.preTraverseDown
{m : Type → Type}
[Monad m]
[MonadLiftT (ST IO.RealWorld) m]
(visitGoal : Aesop.GoalRef → m Bool)
(visitRapp : Aesop.RappRef → m Bool)
(visitMVarCluster : Aesop.MVarClusterRef → m Bool)
:
Aesop.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 : Aesop.GoalRef → m Bool)
(visitRapp : Aesop.RappRef → m Bool)
(visitMVarCluster : Aesop.MVarClusterRef → m Bool)
:
Aesop.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 : Aesop.GoalRef → m Unit)
(visitRapp : Aesop.RappRef → m Unit)
(visitMVarCluster : Aesop.MVarClusterRef → m Unit)
:
Aesop.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 : Aesop.GoalRef → m Unit)
(visitRapp : Aesop.RappRef → m Unit)
(visitMVarCluster : Aesop.MVarClusterRef → m Unit)
:
Aesop.TreeRef → m Unit
Equations
- One or more equations did not get rendered due to their size.