From f0b81ea5678dfab2ecd15c67435ed336e9a0c19a Mon Sep 17 00:00:00 2001
From: Andrew Jeffery <andrew@aj.id.au>
Date: Tue, 2 Aug 2022 02:09:55 +0930
Subject: [PATCH] core: invariants: Fix 'index' typo (#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>
---
 docs/core/invariants.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docs/core/invariants.rst b/docs/core/invariants.rst
index 4fd87ea..ae04884 100644
--- 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.