1
$\begingroup$

Can somebody explain to me the meaning of $::$ in the following predicate?

$$(\forall i : P(i) : Q(i)) \equiv (\forall i :: P(i) \implies Q(i))$$

$\endgroup$
0

1 Answer 1

2
$\begingroup$

"::" is ":" followed by another ":", i.e., two separators.

"$\forall i :: P(i) \implies Q(i)$" is the same as "$\forall i :    : P(i) \implies Q(i)$", i.e, there is no premise/second term. Or you can consider the second term as $\text{true}$ or $\top$.

This situation is similar to the slice notation for lists in Python. For a list A, all four notations A[::3], A[0::3], A[:len(A):3] and A[0:len(A):3] mean the same thing.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.