Question

the standard List type in Coq can be expressed as:

Inductive List (A:Set) : Set :=
  nil : List A
| cons : A -> List A -> List A.

as I understand, W-type express a well-founded tree of elements of this type. so, what if nil is not qualified by A? i.e. we have:

for all A: Set nil : List A

instead of

for all A: Set nil A: List A

is this a correct W-type? can I express this in Coq?

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top