[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

list over the empty type

I am a novice PVS user so my question is probably rather stupid, but
anyway the answer is important. For some reasons I need a type which
corresponds to an instance of a list with actual parameter being an
empty TYPE, i.e. I would like to obtain something like:

T: TYPE  % empty!!!
traces = list[T]

(so the type traces contains only an empty list).

1. Is it possible?
2. If it is possible what consequences I might expect further on?