coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club]specification and Type

From: Lionel Elie Mamane <lionel AT mamane.lu>
To: "Jean.Duprat" <duprat AT ens-lyon.fr>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club]specification and Type
Date: Thu, 2 Mar 2006 12:11:51 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Thu, Mar 02, 2006 at 10:32:55AM +0100, Jean.Duprat wrote:

> Axiom I4 : {A:Point &
>            {B:Point &
>                {C:Point &
>                    (forall D : Line, {~(D A)}+{~(D B)}+{ ~(D C)})
>                }
>            }
>        }.
> but Coq refuses since (forall D : Line, {~(D A)}+{~(D B)}+{ ~(D C)}) has
> type Type when Set is expected.

Use sigT instead of sigS. I never remember the notations and the
manual / standard library on the web is not immediately helpful, but
this should get you going.

--
Lionel

[Coq-Club]specification and Type, Jean.Duprat
- Re: [Coq-Club]specification and Type, Lionel Elie Mamane
- <Possible follow-ups>
- Re: [Coq-Club]specification and Type, Yves Bertot
  - Re: [Coq-Club]specification and Type, Julien Narboux