There was an error while loading. Please reload this page.
1 parent 0aa8d5c commit 60385ccCopy full SHA for 60385cc
1 file changed
Manual/Grind.lean
@@ -1825,7 +1825,7 @@ This needs a mechanism for keeping up to date.
1825
[assign] (values m).size := 0
1826
```
1827
1828
-An immediate problems we can see here is that
+An immediate problem we can see here is that
1829
`grind` does not yet know that `a ∈ m` is the same as `a ∈ m.indices`.
1830
Let's add this fact:
1831
0 commit comments