diff --git a/Manual/Grind.lean b/Manual/Grind.lean index 309e714b..9d29d94c 100644 --- a/Manual/Grind.lean +++ b/Manual/Grind.lean @@ -1825,7 +1825,7 @@ This needs a mechanism for keeping up to date. [assign] (values m).size := 0 ``` -An immediate problems we can see here is that +An immediate problem we can see here is that `grind` does not yet know that `a ∈ m` is the same as `a ∈ m.indices`. Let's add this fact: