Skip to content

Notion of composition on `oFunctor`s, and some renaming

Robbert Krebbers requested to merge robbert/oFunctor into master

Add a notion oFunctor_compose that composes two oFunctors.

The name oFunctor_compose was already in use, for the composition lemma of oFunctor_map. I thus renamed {o,r,ur}Functor_{ne,id,compose,contractive} into {o,r,ur}Functor_map_{ne,id,compose,contractive}, which is also more consistent with the rest of the development (we had names like auth_map_compose, excl_map_compose, etc.).

This is a breaking change /cc @iris-users

Merge request reports