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

[PVS-Help] Sequence initialization

I have a sequence type defined in a record as follows:

  rec: TYPE = [#
    % ...
    slist: [nat -> sequence[nat]]

I'd like to have an initial version of the record where

  slist[0] is a singleton sequence containing the element 0, and
  slist[x > 0] are empty

Does anyone know of the proper syntax to use? Thanks