The Coq mailing list

["Jean.Duprat" <duprat AT ens-lyon.fr>]

Hi,

In plane geometry, where points are elements of a Set (Parameter Point : 
Set.)
and lines are defined as property on points (Definition Line := Point -> 
Prop.),
I would express one of the incidence axiom saying that I can construct three
points, say A, B and C, such that for every line, there exists an 
algorithm for
finding the point among these three points, that does not belong to the 
line.

So I try :
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.

I would know if
- I have written a bad formule, and a correct one will be accepted by Coq,
- this is not possible for a fundamental reason,
- or it is not possible with the current version of Coq.

Thanks

   Jean Duprat