表达式

到目前为止，我们一直在隐式地使用表达式；我们只是没说清楚。对于我们的目的，表达式是任何跟在==，=，:=或\in后面的东西。在本节中，我们将介绍一些通用表达式修饰符。

逻辑联结词

我们已经使用了逻辑联结词有一段时间：/\ (且)，\/( 或)。我们可以把表达式和它们连接起来。一个微妙之处是，这是TLA+对空格敏感的唯一情况。如果你对某一行进行缩进，TLA+将认为这是子句的开始。例如:

/\ TRUE
  \/ TRUE
/\ FALSE \* (T \/ T) /\ F

/\ TRUE
  \/ TRUE
  \/ FALSE \* (T \/ T \/ F)

\/ TRUE
\/ TRUE
  /\ FALSE \* T \/ (T /\ F)

这有几点经验:

• 如果两个逻辑运算符位于相同的缩进级别，那么它们属于相同的表达式级别。
• 如果逻辑运算符位于缩进的更高级别，则它是前面运算符语句的一部分。
• 每个缩进级别只使用一种类型的运算符。

LET-IN

任何表达式都可以使用LET-IN将局部运算符和定义单独添加到该表达式中：

LET IsEven(x) == x % 2 = 0
IN  IsEven(5)

LET IsEven(x) == x % 2 = 0
    Five == 5
IN  IsEven(Five)

LET IsEven(x) == LET Two == 2
                     Zero == 0
                 IN x % Two = Zero
    Five == 5
IN  IsEven(Five)

这里的空格并不重要：我们可以LET IsEven(x) == x % 2 = 0 Five == 5 IN IsEven(Five)，它将正确解析为LET-IN中的两个独立操作符。但是为了易读性，你还是应该使用换行符。

IF-THEN-ELSE

正如你所期望的：

IsEven(x) == IF x % 2 = 0 
             THEN TRUE
             ELSE FALSE

和之前一样，是否对齐并不重要，但是你应该对齐它们，除非你真的讨厌你的同事。

CASE

大多数情况下，情况都是你所期望的一样，但有一个细微的不同：

CASE x = 1 -> TRUE
  [] x = 2 -> TRUE
  [] x = 3 -> 7
  [] OTHER -> FALSE

OTHER的是默认的。如果没有一种情况匹配，而你遗漏了另一种情况，TLC认为这是一个错误。如果有多个匹配项，TLC将为你选择一个，而不是分支。换句话说，就是下面的代码:

CASE TRUE -> FALSE
  [] TRUE -> TRUE

Nesting(嵌套)

表达式的所有部分都是表达式或标识符，因此可以将表达式放在其他表达式中。此外，所有表达式都可以在PlusCal代码中使用。