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
    • One or more equations did not get rendered due to their size.
    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
      • One or more equations did not get rendered due to their size.
      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
        • One or more equations did not get rendered due to their size.
        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
          • One or more equations did not get rendered due to their size.
          Instances For