recursive type

[David Le-Berre <David.Le-Berre@univ-savoie.fr>]

hello

i have a problem to define an abstract syntax of types in pvs

i have a type valuetype wich can be a basetype or a constructedtype

constructedtype wich  can be a connection{value_type}

another problems for me is to say that a type is a subtype of another

for exemple constructed is of type connection{value_type} and also a subtype of value_type

when i try this :

constructed_type : type -> connection[value_type] 
%connection is a datatype
constructed_type : type from value_type

pv is not agree.

thanks for answers