tlaplus_repl157
-------------------------------------------------------------------------------------
 Welcome to the TLA+ REPL! This REPL uses the TLC model checker
 to evaluate TLA+ expressions interactively. It is meant as an
 aid for learning TLA+ and debugging TLA+ specs.
-------------------------------------------------------------------------------------
(TLA+REPL) >>> 3*4
12
(TLA+REPL) >>> {x*2: x \in 1 .. 5}
{2, 4, 6, 8, 10}
(TLA+REPL) >>> CHOOSE x \in 1..4: x > 3
4
(TLA+REPL) >>> quit
Goodbye!