The usage of the vertical bar, '|' in Alloy, and where is the convention from?

Question

For a beginner in Alloy, there seems to be three places to see the vertical bar, '|',

1. In the comprehension,

{x: e | F}

2. In the quantified constraint,

all x: e | A

3. In the let expression,

let x = e | A

Only in the first case of the comprehension in Alloy, the usage of | is the same as the conventional expression of the comprehension. For example, in the set theory, the comprehension is expressed in the same way, too.

However, in the second case, the quantified constraint looks different from the conventional expression in the set theory. For example, in the set theory, the expression is like, . I did not see | been used in this kind of context.

And in the third case, the usage of | also appears to be Alloy's own way.

I mean, in my first impression, it looks confusing to me because I could not find the correct context to orient myself. Do people find it confusing, too? Or is it because of my limited knowledge of the set theory or some convention from other fields?

Answer 1

Take it as what it is: a convention on a notation, which is just here to mark the separation between the range (before |) and the body (after |).

Notice that, even in math and comp sci, there's not a unique convention.