interaction tree
Abstractly, interaction trees are the appropriate adaptation of freer monads to
CoInductive itree (E : Type -> Type) (R : Type) : Type :=
| Ret (r : R)
| Tau (t : itree E R)
| Vis {A : Type} (e : E A) (k : E -> itree E R)
.
Abstractly, interaction trees are the appropriate adaptation of freer monads to
CoInductive itree (E : Type -> Type) (R : Type) : Type :=
| Ret (r : R)
| Tau (t : itree E R)
| Vis {A : Type} (e : E A) (k : E -> itree E R)
.