Re: [tlaplus] How do I extract particular mapping from each element in a set?

 Not sure I understand correctly what you are after but how about the following (assuming that all value' [or val'?] fields indeed hold pairs):get(t) ==  LET filtered == {el \in elements : el.key > t}  IN  {el.value : el \in filtered}TLA+ offers two forms of set comprehension (generalized to several variables):  { x \in S : P(x) }  computes the subset of S whose elements satisfy the predicate P  { f(x) : x \in S }   yields the result of applying f to all elements of S (analogous to map in functional programming)The set _expression_ in your original definition of get matches neither of these forms.StephanOn 2 Apr 2019, at 22:53, Balaji Arun wrote:I have a set of functions, and I want to extract a particular mapping from each element in the set. I tried the following, but dint work.get(t) == {<>: \A element \in elements: element.key > t => <> \in element.value}I get a syntax error at \A. So, I tried to split them as:get1(t) == {element \in elements: element.key > t}get2(t) == {element.value : element \in get1(t)}get3(t) == {val : val \in get2(t)}get4(t) == {<> : <> \in val}and combined it into: committed(t) == {<> : <> \in {val : val \in {element.val : element \in {element \in elements: element.key > t}}}}Is this correct? Can this be simplified further?Thanks! -- 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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx. Visit this group at https://groups.google.com/group/tlaplus. For more options, visit https://groups.google.com/d/optout. -- 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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx. Visit this group at https://groups.google.com/group/tlaplus. For more options, visit https://groups.google.com/d/optout.

• Follow-Ups:
• References: