coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club]Setoid for arbitrary relation?

From: Frederic Blanqui <blanqui AT loria.fr>
To: Claudio Sacerdoti Coen <sacerdot AT cs.unibo.it>
Cc: "Koprowski, A." <A.Koprowski AT tue.nl>, coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club]Setoid for arbitrary relation?
Date: Thu, 22 Mar 2007 09:28:32 +0100 (CET)
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Wed, 21 Mar 2007, Claudio Sacerdoti Coen wrote:

Yes, it is. However, the type of union in the standard library is

forall A, relation A -> relation A -> A -> A -> Prop

To be handled correctly it should be

forall A, relation A -> relation A -> relation A.

can't you modify the standard library? it would be better.

[Coq-Club]Setoid for arbitrary relation?, Koprowski, A.
- Re: [Coq-Club]Setoid for arbitrary relation?, Claudio Sacerdoti Coen
  - Re: [Coq-Club]Setoid for arbitrary relation?, Frederic Blanqui
  - RE: [Coq-Club]Setoid for arbitrary relation?, Koprowski, A.
- <Possible follow-ups>
- Re: [Coq-Club]Setoid for arbitrary relation?, Santiago Zanella