Re: [tlaplus] Record: test for field

[Stephan Merz <stepha...@xxxxxxxxx>]

Assuming you have a constant null that you'd like to return as a default value, you can define an operator such as

AccessField(r,f) ==
  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.

Regards,
Stephan

> 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.