The Coq mailing list

[Henri Fraisse <henri.fraisse AT trusted-logic.fr>]

Bonjour,

A ma grande surprise je me suis rendu compte que les fonctions ayant pour type "Type->A"
pouvaient etre appliquees a des objets de type "Set" tels que "nat",  ou des objets de type Prop tels que "O=O".

Cela semble faire de "Set "et "Prop" des sous-types de "Type", alors que jusque -la je les voyais
essentiellement comme des objets de type Type.

Du coup, je me demande si on aurait pas interet a formaliser d'abord dans la sorte "Type"
avant de particulariser a Prop ou a Set.

Par exemple, il est facile de montrer le lemme suivant: (A:Set)(a1,a2:A)a1=a2<->a1==a2.
Intuitivement, il me semble que "eqT" est par consequent une stricte généralisation de "eq".

De meme, je me demande pourquoi on ne definit pas le type "list" de la facon suivante:

Inductive Tlist[T:Type]:Set := tnil:(Tlist T) | tcons:T->(Tlist T)->(Tlist T).

ce qui permettrait de construire non seulement des listes d'entiers mais aussi des listes de propositions
ou de types.

Evidemment j'imagine qu'il doit y avoir quelque chose qui cloche mais je ne vois pas quoi.

Quelqu'un pourrait-il m'eclairer sur ce point la?

merci d'avance,

-- 
=========================================================================

Henri Fraisse

+----------------------------------+------------------------------------+
| Henri FRAISSE                    |      TRUSTED LOGIC S.A.            |
| Henri.Fraisse AT trusted-logic.fr   |                                    |
| Phone: +33 01 30 97 25 04        |     5, rue du Bailliage,           |
| Secr.: +33 01 30 97 25 00        |       78000 Versailles             |
| Fax:   +33 01 30 97 25 19        |           FRANCE                   |
+----------------------------------+------------------------------------+