Hi all,
I can filter a set of functions to contain just the surjective functions like this:
{m \in [1..2 -> 3..4] : \A j \in 3..4 : \E i \in DOMAIN m: m[i] = j}
yielding the expected result:
{<<3, 4>>, <<4, 3>>}
When I try the same filtering with surjective records:
{m \in [a: 3..4, b: 3..4] : \A j \in 3..4 : \E i \in DOMAIN m: m.i = j}
the following error message is displayed:
The `Evaluate Constant _expression_� section�s evaluation failed.
Attempted to apply the operator overridden by the Java method
public static tlc2.value.impl.Value tlc2.module.TLC.PrintT(tlc2.value.impl.Value),
but it produced the following error:
Attempted to select nonexistent field "i" from the record
[a |-> 3, b |-> 3]
m.i
What is the reason for this different behaviours?
Advices are appreciated,
Siegfried Bublitz
--
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/CAL%2B9cEp8ke8AcfpRHfrazmcOSuPcv6Ac5bvXGuvMVYRXR0mr3g%40mail.gmail.com.