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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4351c96e-420c-40f5-b5b4-5ed42fa131dcn%40googlegroups.com.
On 3 Dec 2022, at 18:21, Alan Munirji <munir...@gmail.com> wrote:
Hey Stephan, first off thank you for the timely response. I didn't want to give you a partial response so I've been working through the problem a little bit each day and I gave your suggestion a bit of a go but couldn't seem to figure out where my issue is. I think I should try to create a minimum reproducible example and go from there.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8b21fdc2-fe19-40d4-ab34-52205ce90ad9n%40googlegroups.com.