| Thanks, Stephan; that was a help. The _expression_ you suggested didn’t quite work because it needed square brackets around “X -> Nodes”, and TLC couldn’t enumerate the values, but once you showed me what the problem was, I was able to define and use this constant: SetsOfLabeledEdges == UNION { [ 1..n -> Nodes ] : n \in 0..Cardinality(Nodes) } 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/3A716915-90B6-461C-AD59-585B5A5AD6B6%40TimLeonard.us. |