Documentation

Aesop.Tree.Traversal

@[specialize #[]]
partial def Aesop.traverseDown {m : TypeType} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (visitGoalPre : Aesop.GoalRefm Bool) (visitGoalPost : Aesop.GoalRefm Unit) (visitRappPre : Aesop.RappRefm Bool) (visitRappPost : Aesop.RappRefm Unit) (visitMVarClusterPre : Aesop.MVarClusterRefm Bool) (visitMVarClusterPost : Aesop.MVarClusterRefm Unit) :
@[specialize #[]]
partial def Aesop.traverseUp {m : TypeType} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (visitGoalPre : Aesop.GoalRefm Bool) (visitGoalPost : Aesop.GoalRefm Unit) (visitRappPre : Aesop.RappRefm Bool) (visitRappPost : Aesop.RappRefm Unit) (visitMVarClusterPre : Aesop.MVarClusterRefm Bool) (visitMVarClusterPost : Aesop.MVarClusterRefm Unit) :
@[inline]
def Aesop.preTraverseDown {m : TypeType} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (visitGoal : Aesop.GoalRefm Bool) (visitRapp : Aesop.RappRefm Bool) (visitMVarCluster : Aesop.MVarClusterRefm Bool) :
Equations
Instances For
    @[inline]
    def Aesop.preTraverseUp {m : TypeType} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (visitGoal : Aesop.GoalRefm Bool) (visitRapp : Aesop.RappRefm Bool) (visitMVarCluster : Aesop.MVarClusterRefm Bool) :
    Equations
    Instances For
      @[inline]
      def Aesop.postTraverseDown {m : TypeType} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (visitGoal : Aesop.GoalRefm Unit) (visitRapp : Aesop.RappRefm Unit) (visitMVarCluster : Aesop.MVarClusterRefm Unit) :
      Equations
      Instances For
        @[inline]
        def Aesop.postTraverseUp {m : TypeType} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (visitGoal : Aesop.GoalRefm Unit) (visitRapp : Aesop.RappRefm Unit) (visitMVarCluster : Aesop.MVarClusterRefm Unit) :
        Equations
        Instances For