Skip to content
GitLab

Kill `{o,r,ur}Functor_diag` coercions, and rename into `{o,r,ur}Functor_apply`

Merged Robbert Krebbers requested to merge robbert/functor_diag into master

Various reasons for doing this:

  • Most of the time we are interested in oFunctor_car, so it's really confusing that oFunctor_diag is a coercion
  • The coercion doesn't work well with the Cofe type class argument (see !257 (merged))---an underscore _ is needed when applying the coercion.
  • The coercion is very little used, so better to be explicit, especially in light of #240 (closed).

/cc @iris-users This is a breaking change.

This MR closes issue #240 (closed).

Edited by Robbert Krebbers