You have misunderstood why
A stands there in the definition of list.
Let us first look at how we might define lists of booleans:
Inductive ListBool : Set :=
| nilBool : ListBool
| consBool : bool -> ListBool -> ListBool.
And here is how we might define lists of natural numbers:
Inductive ListNat : Set :=
| nilNat : ListNat
| consNat : nat -> ListNat -> ListNat.
As you can see the
nilNat are constants that do not depend on any parameters. It is boring to define lists of booleans, lists of natural numbers, lists of lists of booleans, etc. Coq allows a parametrized definition of lists in which the
List type itself takes a parameter
A as input, to give lists of elements of type
A. This is defined as you wrote:
Inductive List (A : Set) : Set :=
| nil : List A
| cons : A -> List A -> List A.
nil clause we have
List A. Here
A is the argument to
List, it is not an argument to
nil. If we wrote just
List then Coq would ask "list of what"? For a similar reason the
cons constructor has two occurences of
Let me put it another way. The type of
Set. The type of
Set -> Set. So we have to apply
List to a set before we get a list.