Re: [PVS-Help] Sequence initialization

[Natarajan Shankar <shankar@xxxxxxxxxxx>]

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
something like 

slist := (LAMBDA (i:nat): IF i = 0 THEN
                                 (# length := 1,
				    seq := (LAMBDA (j: below(1)): 0)
				  #)
		           ELSE empty_seq ENDIF)

-Shankar			   

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[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
> 
> jerome