From 6cefbc4bb0a9ca6163075877f2d0ef30d6ec406a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Thu, 4 Sep 2025 09:05:00 -0700
Subject: [PATCH] chore: fix typo (#10251)

---
 src/Init/Grind/Attr.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Grind/Attr.lean b/src/Init/Grind/Attr.lean
index 8ec9ef46bb..0d9d327ecf 100644
--- a/src/Init/Grind/Attr.lean
+++ b/src/Init/Grind/Attr.lean
@@ -95,7 +95,7 @@ Ordinarily, the grind attribute does not consider the `=` symbol when generating
 -/
 syntax grindEqBwd  := patternIgnore(atomic("←" "=") <|> atomic("<-" "="))
 /--
-The `→` modifier instructs `grind` to select a multi-pattern from the conclusion of theorem.
+The `←` modifier instructs `grind` to select a multi-pattern from the conclusion of theorem.
 In other words, `grind` will use the theorem for backwards reasoning.
 This may fail if not all of the arguments to the theorem appear in the conclusion.
 -/