The Coq mailing list

[Casteran Pierre <pierre.casteran AT labri.fr>]

Le 21/06/2013 11:03, Casteran Pierre a écrit :
> Hi,
>
>    I met some problems with the "join" function.
> using Cédric définitions (taken from Cocorico),
> everything seems OK until I try to apply join to
> an instance of an inductive family of types.
>
> Happily, bind, return are OK, but a simple application
> of join gives me a universe inconsistency.
>
> Perhaps it's the definition of the MM family that is wrong ?
> Is there some standard way to solve this issue ?
>
> Pierre


It works better if the definition of the Monad class
takes bind and return_ as parameters:

Class Monad' (m : Type -> Type) (return_ : forall A, A -> m A)
 (bind : forall A, m A -> forall B, (A -> m B) -> m B): Prop :=
{
 (* some place for laws *)}.

Sorry for the spam.

Pierre