hwayne / learntla

A TLA+ guide
http://www.learntla.com
Creative Commons Attribution 4.0 International
278 stars 57 forks source link

[tla/tuples] `<<2, "a">> \notin chessboard_squares` example fails #90

Closed zed closed 4 years ago

zed commented 4 years ago

Error message:

The `Evaluate Constant Expression� section�s evaluation failed.
Attempted to check equality of string "a" with non-string:
2

I've tested in TLA+ Toolbox 1.6.0 using expression ("No Behavior Spec"):

LET chessboard_squares == {"a", "b", "c", "d", "e", "f", "g", "h"} \X (1..8)
IN 
/\ <<"a", 2>> \in chessboard_squares
/\ <<2, "a">> \notin chessboard_squares
/\ <<"b", 10>> \notin chessboard_squares

Removing <<2, "a">> fixes the expression.