inductive Aesop.TreeRef : Type

• 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

• Aesop.preTraverseDown visitGoal visitRapp visitMVarCluster = Aesop.traverseDown visitGoal (fun x => pure ()) visitRapp (fun x => pure ()) visitMVarCluster fun x => pure ()

@[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

• Aesop.preTraverseUp visitGoal visitRapp visitMVarCluster = Aesop.traverseUp visitGoal (fun x => pure ()) visitRapp (fun x => pure ()) visitMVarCluster fun x => pure ()

@[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

• Aesop.postTraverseDown visitGoal visitRapp visitMVarCluster = Aesop.traverseDown (fun x => pure true) visitGoal (fun x => pure true) visitRapp (fun x => pure true) visitMVarCluster

@[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

• Aesop.postTraverseUp visitGoal visitRapp visitMVarCluster = Aesop.traverseUp (fun x => pure true) visitGoal (fun x => pure true) visitRapp (fun x => pure true) visitMVarCluster