core: invariants: Fix 'index' typo (hwayne#34)

Make the inline TypeInvariant code match the code in the example at docs/specs/duplicates/inv_1/duplicates.tla. Signed-off-by: Andrew Jeffery <andrew@aj.id.au>
simondorfman · Aug 1, 2022 · f0b81ea · f0b81ea
1 parent 63aeb60
commit f0b81ea
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/docs/core/invariants.rst b/docs/core/invariants.rst
@@ -71,7 +71,7 @@ So back to the nature of the invariant. We say ``is_unique`` is the boolean type
   TypeInvariant ==
     /\ is_unique \in BOOLEAN
     /\ seen \subseteq S
-    /\ i \in 1..Len(seq)+1
+    /\ index \in 1..Len(seq)+1
 
 I think that's enough of an introduction to invariants. Now let's write one that proves our algorithm correct.