Fundamentally, you are trying to convert a set to a sequence that contains each element of the set exactly once. The module SequenceExt from the Community Modules contains an operator that does that:IsInjective(s) == \A i, j \in DOMAIN s: (s[i] = s[j]) => (i = j)SetToSeq(S) == CHOOSE f \in [1..Cardinality(S) -> S] : IsInjective(f)Now you can define your operator as follows:tableInit ==  [person \in group |->      [ status |-> "Active",        divisions |-> LET divs == SetToSeq(getDivisions(person))                      IN  { [id |-> i, assignedDivision |-> divs[i]] :                            i \in 1 .. Len(divs) } ]]Instead of representing divs' as a set of records with id fields, you could represent it as a sequence where the id is implicit in the position of the element in the sequence. However, I wonder if you are at the right level of abstraction for your specification: all the information that you need is contained in the set group' and the operator `getDivisions'. Is it important to construct an explicit data structure that materializes that information, in particular since you don't care about the order of IDs?StephanOn 11 Nov 2020, at 06:53, tlalearner wrote:I have a very simple initialization for a function as follows:sampleTableINIT ==        sampleTable = [person \in group |->             [                status |-> "Active",                divisions |-> {[assignedDivision |-> division] : division \in getDivisions(person)}             ]]Here is a sample result from the definition:[Sam :> [status |-> "Active", divisions |-> { [assignedDivision |-> "Sales"]]  [Mary :> [status |-> "Active", divisions |-> { [assignedDivision |-> "Sales"], [assignedDivision |-> "CS" }]What I'd like to accomplish is simple: Per person entry, I'd like to assign an ID per division. The result below is what I want:[Sam :> [status |-> "Active", divisions |-> { [id |-> 1, assignedDivision |-> "Sales"]]    [Mary :> [status |-> "Active", divisions |-> { [id |-> 1, assignedDivision |-> "Sales"], [id |-> 2, assignedDivision |-> "CS" }]  Order on ID assignment does not matter. Is there an easy way to do this rather than mutating the function in a future state? -- 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/5c1eb8c4-80d2-472f-a3cd-fe6147adabean%40googlegroups.com. -- 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/31E8E255-2AE2-4152-ACB9-9128F40E1704%40gmail.com.