Documentation

Aesop.Tree.Traversal

source
inductive Aesop.TreeRef :
Type
Instances For
    source
    @[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
    source
    @[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
    source
    @[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
      Instances For
        source
        @[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
          Instances For
            source
            @[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
              Instances For
                source
                @[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
                  Instances For