One is able to use a constant in the type of a constant or a type in a definition instead of a type constructor, as in the following code:
Kind pair type -> type -> type.
Type pair_c A -> B -> pair A B.
Kind foo type -> type.
Type foo1 list (pair_c A A) -> foo A.
Type foo2 list (pair A A) -> foo A.
Define bar : list (pair_c A A) -> prop by
bar L.
The constant foo1 is defined to have arguments of type list (pair_c A A), where pair_c is a constant, not a type constructor. The constant foo2 is the version which is intended. The same happens with the definition of bar.
This only appears to happen when the constant is nested inside a type constructor. For example, the definition
Type foo3 pair_c A A -> foo A.
fails with the error
Error: Unknown type constructor: pair_c
The definition
Define baz : list (pair_c A A) -> prop by
baz (P::Tl).
also fails, apparently since the variable P would have the non-type type pair_c A A.
One is able to use a constant in the type of a constant or a type in a definition instead of a type constructor, as in the following code:
The constant
foo1is defined to have arguments of typelist (pair_c A A), wherepair_cis a constant, not a type constructor. The constantfoo2is the version which is intended. The same happens with the definition ofbar.This only appears to happen when the constant is nested inside a type constructor. For example, the definition
fails with the error
The definition
also fails, apparently since the variable
Pwould have the non-type typepair_c A A.