Thanks a lot.
On Wednesday, August 8, 2018 at 10:54:49 PM UTC+8, Stephan Merz wrote:
Hello,
your approach is correct. Instead of checking emptiness via cardinality, I’d rather use a direct set comparison. Also, you can avoid some repetition using a LET definition, like so:
get_element(key) ==
LET matches == { x \in some_set : x.key = key }
IN IF matches = {} THEN [ key |-> 0 ]
ELSE CHOOSE m \in matches : TRUE
Regards,
Stephan
> On 8 Aug 2018, at 12:42, wang...@xxxxxxxxx wrote:
>
> I'm using CHOOSE, but it will catch error when no element is satisfied by p.
>
> In my situation, I want to choose one element from a set or get a default element.
>
> Like this:
>
> ```
> some_set == {[key |-> 1, x |-> 1], [key |-> 2, x |-> 3], ...}
>
> get_element(key) ==
> IF Cardinality({x \in some_set : x.key = key}) /= 0
> THEN CHOOSE x \in some_set : x.key = key
> ELSE [x |-> 0]
>
> val == get_element(9).x
> ```
>
> Is there a shorter way to represent `get_element`?
>
> --
> 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+u...@googlegroups.com.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.