[PVS-Help] dependent types in pvs

[Martin Hofmann <hofmann@xxxxxxxxxx>]

 Dear experts,

 is it possible to postulate an unknown type valued function in PVS?

 When I write something like

 types : THEORY
 BEGIN
    Types : TYPE+
    semof : [Types -> TYPE+]
 End

 then PVS complains with a syntax error.

 My aim is to specify systems that have wires and functional components 
 and every wire has a type
 such as boolean or 32bit-word or whatever and then the semantics of the 
 system would assign to each time t:posnat and wire w a value of the type 
 assigned to that wire.

 Thanks in advance, Martin