Skip to content

Make IForest's bind associative #240

@Lysxia

Description

@Lysxia

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

No one assigned

    Labels

    enhancementNew feature or requestitreesParticular to theory and implementation of itrees

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions