[tlaplus] How can I define a sequence as part of a record's fields?

[Alan Munirji <munirjialan@xxxxxxxxx>]

From Specifying Systems, I read in section 4.1 that:

"The Sequences module defines the following operators on sequences: 

Seq(S) 

The set of all sequences of elements of the set S. For example, h3, 7i is an element of Seq(Nat)."

I thought then that I could have a sequence as a field of a record by doing:

MyRec == [

    id: recs,

    seek: Seq(Nat)

]

but it doesn't work, stating:

Attempted to enumerate a set of the form [l1 : v1, ..., ln : vn],

but can't enumerate the value of the 'seek' field:

Seq(Nat)

(Eventually, I'd like to initialize this record's seek field to be <<>> in the init state, and then use it to track ordered operations.)

I am very new to TLA+, any help would be so appreciated.

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4351c96e-420c-40f5-b5b4-5ed42fa131dcn%40googlegroups.com.