[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] Sequence initialization
Jerome: Since sequence[T] is just [nat -> T],
you can write sequence[sequence[nat]] for
[nat -> sequence[nat]].
I'm not sure what you mean by a singleton sequence. It's possible that
you mean finite sequences, which is a record with length and seq.
If you want sequence[finseq[nat]], then the initialization would be
slist := (LAMBDA (i:nat): IF i = 0 THEN
(# length := 1,
seq := (LAMBDA (j: below(1)): 0)
ELSE empty_seq ENDIF)
Jerome <jerome@xxxxxxxxxxxxxx> wrote:
> 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 is a singleton sequence containing the element 0, and
> slist[x > 0] are empty
> Does anyone know of the proper syntax to use? Thanks