Thank you so much for creating this website!
In the "Parameterizing Specs" chapter,
Is there significance to leaving the s parameter on the IsUnique operator?
IsUnique(s) ==
\A i, j \in 1..Len(s):
- i # j => s[i] # s[j]
+ i # j => seq[i] # seq[j] Since the operator no longer depends on s (since Len(s) = Len(seq)), is there any reason why we should not drop the entire parameter?
- IsUnique(s) ==
- \A i, j \in 1..Len(s):
- i # j => s[i] # s[j]
+ IsUnique ==
+ \A i, j \in 1..Len(seq):
+ i # j => seq[i] # seq[j]
I'm not sure if this is stylistic, or is a requirement for TLA+.
Thank you so much for creating this website!
In the "Parameterizing Specs" chapter,
Is there significance to leaving the
sparameter on theIsUniqueoperator?IsUnique(s) == \A i, j \in 1..Len(s): - i # j => s[i] # s[j] + i # j => seq[i] # seq[j]Since the operator no longer depends on
s(sinceLen(s) = Len(seq)), is there any reason why we should not drop the entire parameter?I'm not sure if this is stylistic, or is a requirement for TLA+.