coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Arnaud Spiwack <arnaud.spiwack AT gmail.com>
- To: Guillaume Melquiond <guillaume.melquiond AT inria.fr>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Notation for functional relation
- Date: Mon, 27 Jan 2014 16:13:44 +0100
>> 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.
I'm confused. Apart from the fact that I forgot an obvious lambda (f is supposed to be of type A->B->(X->Prop)), this definition is a correct binary extension for the powerset monad. Could you elaborate on the issue you have with it?
>
> Best regards,
>
> Guillaume
>
- [Coq-Club] Notation for functional relation, Anders Lundstedt, 01/26/2014
- Re: [Coq-Club] Notation for functional relation, Arnaud Spiwack, 01/27/2014
- Re: [Coq-Club] Notation for functional relation, Guillaume Melquiond, 01/27/2014
- Re: [Coq-Club] Notation for functional relation, Arnaud Spiwack, 01/27/2014
- Re: [Coq-Club] Notation for functional relation, Arnaud Spiwack, 01/27/2014
- Re: [Coq-Club] Notation for functional relation, Guillaume Melquiond, 01/27/2014
- Re: [Coq-Club] Notation for functional relation, Arnaud Spiwack, 01/27/2014
- Re: [Coq-Club] Notation for functional relation, Rui Baptista, 01/27/2014
- Re: [Coq-Club] Notation for functional relation, Arnaud Spiwack, 01/27/2014
- Re: [Coq-Club] Notation for functional relation, Daniel Schepler, 01/28/2014
- Re: [Coq-Club] Notation for functional relation, Arnaud Spiwack, 01/28/2014
- Re: [Coq-Club] Notation for functional relation, Daniel Schepler, 01/28/2014
- Re: [Coq-Club] Notation for functional relation, Arnaud Spiwack, 01/28/2014
- Re: [Coq-Club] Notation for functional relation, Daniel Schepler, 01/28/2014
- Re: [Coq-Club] Notation for functional relation, Arnaud Spiwack, 01/28/2014
- Re: [Coq-Club] Notation for functional relation, Guillaume Melquiond, 01/27/2014
- Re: [Coq-Club] Notation for functional relation, Arnaud Spiwack, 01/27/2014
Archive powered by MHonArc 2.6.18.