While Leslie's suggestion is a great way to mix apples and oranges in general, your motivating example was of a special case, where a specific "null" value is required (if you know a language like Haskell, you can compare these two scenarios to an Either type vs a Maybe type, where the latter is asymmetric in the sense that you can have any number of apples but only one orange). In that case, a simpler approach may be to define:BPvalue == (MIN_BP..MAX_BP)NoValue == CHOOSE x : x \notin BPvalueBPmeasurement == {NoValue} \cup BPvalueFrom a theoretical point of view, it is then possible to know that NoValue is not equal to any BPvalue. In practice, when using TLC, you then override NoValue with a "model value" which is comparable with any value and equal to nothing but itself.--
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@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 .