Rust 求值器 step step 实现 [定义] 一步归约 的规则。Rust 的 match match 按顺序尝试分支，这本身是一种“优先级”，而求值规则没有写这种优先级。为什么这样写不会改变语义？因为 [定理] 确定性 的证明已经说明，对每个 $𝑡$ 至多一条规则适用，所以按什么顺序试结果都一样。没有那条定理，“先试 E-PredSucc 再试 E-Pred”就是一个偷偷加进来的、规则里没有的决定。