Surjective functions as records

[Siegfried Bublitz]

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

[Stephan Merz]

I haven't tried this but the domain of your record is {"a", "b"}, so I'd try to write 

\E i \in DOMAIN m : m[i] = j

just as for functions. Remember that records *are* functions.

Stephan

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAL%2B9cEp8ke8AcfpRHfrazmcOSuPcv6Ac5bvXGuvMVYRXR0mr3g%40mail.gmail.com.

[Hillel Wayne]

The reason it didn't work before is that m.i is syntax sugar for m["i"], not m[i].

H

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/0CDC608E-8F9B-4D64-93FE-F95C20FC27CA%40gmail.com.

[Siegfried Bublitz]

This works, thank you, Stephan + Hillel

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAJ-b8sx4HG5X82b41yikereaPpG%2BNWatKfH56BCizMT0%3DDPOew%40mail.gmail.com.