The Coq mailing list

[Matej Kosik <kosik AT fiit.stuba.sk>]

Hello,

I would like to ask a simple question that puzzled me.

In Coq, the `list' function has the type `Type -> Type'. This means that
whenever apply some value whose type can be converted to `Type', I will
get a value whose type is `Type'.

If I take some terms whose type is `Type', this theory holds:

        Coq < Check list Set.
        list Set
             : Type

        Coq < Check list Prop.
        list Prop
             : Type

The conversion rule and the fact that `Set' can be converted to `Type'
also allows me to use terms such as `nat', `bool' as parameters of the
`list' function:

        Coq < Check list nat.
        list nat
             : Set

        Coq < Check list bool.
        list bool
             : Set

There is, however, one thing I do not understand. How could the type of
the whole term (`list nat' or `list bool') be `Set' instead of `Type' as
the type of the `list' function suggests?

Thanks in advance for the answers.