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

*From*: Brian Beckman <bc.be...@xxxxxxxxx>*Date*: Thu, 5 Nov 2015 17:28:07 -0800 (PST)

I wanted to group my vars roughly as follows

then to write

as usual. It doesn't work unless I write

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?

`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?

**Follow-Ups**:**Re: Concatenating tuples of vars for subscript of Next and WF***From:*Leslie Lamport

- Prev by Date:
**Re: [tlaplus] Toolbox 1.5.1 / PDF Internal Viewer on hangs OS X El Capitan** - Next by Date:
**Re: Concatenating tuples of vars for subscript of Next and WF** - Previous by thread:
**RE: [tlaplus] Re: 2016 TLA+ Workshop** - Next by thread:
**Re: Concatenating tuples of vars for subscript of Next and WF** - Index(es):