Is this a well founded inductive type? Can I express this in Coq?
-
31-10-2019 - |
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