[tlaplus] Surjective functions as records

[Siegfried Bublitz <sbublitz24@xxxxxxxxx>]

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.