[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Record: test for field
Assuming you have a constant null that you'd like to return as a default value, you can define an operator such as
IF f \in DOMAIN r THEN r[f] ELSE null
and then write AccessField(r, "A") instead of r["A"]. Remember that records are functions.
> On 29 Jan 2019, at 07:59, Philipp Frank <phil....@xxxxxx> wrote:
> Given a record
> r == [C |-> "B"]
> how can I use a "default" / fallback value for non-existing keys?
> Currently, using r["A"] results in a runtime error 'Attempted to apply the record[C |-> "B"] to nonexistent record field A.'
> 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...@xxxxxxxxxxxxxxxx.
> 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.