search

DeepSpec / InteractionTrees

A Library for Representing Recursive and Impure Programs in Coq
MIT License
204 stars 51 forks source link

Make `IForest`'s bind associative #240

Open Lysxia opened 2 years ago

Lysxia commented 2 years ago

https://github.com/DeepSpec/InteractionTrees/blob/master/extra/IForest.v#L70

Trick: define a coinductive relation relbind : itree E A -> (A -> itree E B -> Prop) -> itree E B -> Prop