alloy - 合金中的高阶量化

Question

我正在阅读有关合金中高阶量化的内容，并看到以下内容：lone p: some X| F
现在，如果关键字“some”修改 p 或​​ X，我感到困惑。这是否意味着 X 应该是非空的，或者是否意味着 p 的基数应该 >=1。

Answer 1

在这种情况下，“some”修改了“X”，这意味着 X 应该是非空的。然而，“lone”仍然修改“p”，意味着 p <= 1 的基数。换句话说，这个约束表示在非空集合“X”中最多有一个“p”，使得“F”成立。