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

Concatenating tuples of vars for subscript of Next and WF



I wanted to group my vars roughly as follows

group1 == <<x, y, z>>
group2
== <<a, b, c>>

vars
== group1 \o group2 \* small circle is tuple concatenation

then to write

Spec == Init /\ [][Next]_vars

as usual.  It doesn't work unless I write

vars == <<x, y, z, a, b, c>>

manually concatenating the tuples and, worse, repeating myself.  Of course, in my real code, as opposed to this toy question, there are many variables with long names and the value of grouping them will be painfully obvious.  My question is about the proper way to use the groups in constructing a term I can use for subscripting formulas.

Did I misunderstand tuple concatenation?