The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 27/01/2014 07:00, Arnaud Spiwack wrote:

> And the binary /monadic extension/ is
>
> Definition extension2 f x y := exists a, exists b, x a -> x b -> f a b

Unfortunately no.

In Why3, we display a warning whenever the user writes this kind of 
predicate ; it has been helpful to debug some broken specifications 
early. It might be worth having the same warning message in Coq.

Best regards,

Guillaume