How to set a default for CHOOSE?

[wangq...@gmail.com]

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

[Stephan Merz]

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

> --
> 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...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

[Qd Wang]

Thanks a lot.