-
Notifications
You must be signed in to change notification settings - Fork 56
Open
Labels
enhancementNew feature or requestNew feature or requestitreesParticular to theory and implementation of itreesParticular to theory and implementation of itrees
Description
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
Metadata
Metadata
Assignees
Labels
enhancementNew feature or requestNew feature or requestitreesParticular to theory and implementation of itreesParticular to theory and implementation of itrees