Significance of Parameter-less Operators?

[iinuwa]

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+.

[hwayne]

I’ll have to go over the chapter again (probably this summer?) but no, there is no need to preserve the parameter.

�

H

�

From: Isaiah Inuwa @.> Sent: Monday, March 24, 2025 2:49 PM To: hwayne/learntla-v2 @.> Cc: Subscribed @.***> Subject: [hwayne/learntla-v2] Significance of Parameter-less Operators? (Issue #94)

�

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?