[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] TLC doesn't like multiple types on function range


Is it possible to define a function with a multiple "type" range like [Nat -> Nat \union BOOLEANwithout TLC complaining about the type?.
When checking a type invariant will result in:

Attempted to check if the value:
is in the integer interval 0..2

If "{a,b}" are untyped model values then there is no problem with [Nat -> Nat \union {a,b}], since "a" and "b" are by definition
unequal to anything but itself. But in the case of BOOLEAN, TLC refuses to compare with anything of different type.


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@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a7fc436e-e2d6-4527-882e-3dcae49c8716o%40googlegroups.com.