source
inductive Aesop.TreeRef :
Type

- goal (gref : GoalRef) : TreeRef
- rapp (rref : RappRef) : TreeRef
- mvarCluster (cref : MVarClusterRef) : TreeRef

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