Hi,Did you receive an answer to this yet? In case you did not, what you are seeing is the pretty printer reducing the first _expression_ to a shorter sequence representation.The term "<<1, 1>>", which is a sequence, is the set of mappings 1 to 1 and 2 to 1, which is equivalent to "(1:>1 @@ 2:>1)". In this case, the pretty printer realizes that the left-hand sides of the mappings are the same as what they would be in a sequence and reduces the output to sequence form.It think if you evaluated "{(1:>1 @@ 2:>1), (1:>1 @@ 2:>2), (1:>2 @@ 2:>1), (1:>2 @@ 2:>2)}" it would print the set of sequences you saw. (I don't have the toolbox handy to check myself, but I think it would do that.)Hope my information is accurate and helps you,RobertOn Sat, Aug 18, 2018 at 1:05 AM Hengfeng Wei <heng...@xxxxxxxxx> wrote:--Hi,I evaluate [{1,2} -> {1,2}] in "Evaluate Constant _expression_"and obtain an unexpected result: {<<1, 1>>, <<1, 2>>, <<2, 1>>, <<2, 2>>}.The _expression_ [{1,3} -> {1,3}] gives the expected result:{ (1 :> 1 @@ 3 :> 1),(1 :> 1 @@ 3 :> 3),(1 :> 3 @@ 3 :> 1),(1 :> 3 @@ 3 :> 3) }.I am using the latest TLA+ Toolbox (Version 1.5.7 of 18 July 2018).What are wrong with my evaluations?
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 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 .