Higher Order quantification in Alloy

Question

I was reading about higher order quantification in alloy, and saw the following: lone p: some X| F
now, I am confused if the keyword 'some' modifies p or X. Does it mean X should be nonempty or does it mean that the cardinality of p should be >=1.

Answer 1

In this case, "some" modifies "X", meaning that X should be non-empty. However, "lone" still modifies "p", implying that the cardinality of p <= 1. In other words, this constraint says that there's at most one "p" in the non-empty set "X" such that "F" holds true.