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

*From*: Alan Munirji <munirjialan@xxxxxxxxx>*Date*: Wed, 30 Nov 2022 19:27:02 -0800 (PST)

From Specifying Systems, I read in section 4.1 that:

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.

**Follow-Ups**:**Re: [tlaplus] How can I define a sequence as part of a record's fields?***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] simple toy theorem** - Next by Date:
**Re: [tlaplus] How can I define a sequence as part of a record's fields?** - Previous by thread:
**Re: [tlaplus] simple toy theorem** - Next by thread:
**Re: [tlaplus] How can I define a sequence as part of a record's fields?** - Index(es):