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