Closed t6s closed 1 year ago
This PR generalizes the factory isMonad_ret_bind in hierarchy.v to be applicable to M : Type -> Type, not only to M : functor.
isMonad_ret_bind
M : Type -> Type
M : functor
Note that there is also the impredicative_set subdir to update (you can use meld maybe).
This PR generalizes the factory
isMonad_ret_bind
in hierarchy.v to be applicable toM : Type -> Type
, not only toM : functor
.