Skip to content

Commit dd9037b

Browse files
authored
doc: typo in grindDef docstring
1 parent 14d76cc commit dd9037b

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Init/Grind/Attr.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -130,7 +130,7 @@ If `grind!` is used, then only minimal indexable subexpressions are considered.
130130
syntax grindLR := patternIgnore("⇒" <|> "=>")
131131
/--
132132
The `.` modifier instructs `grind` to select a multi-pattern by traversing the conclusion of the
133-
theorem, and then the hypotheses from eft to right. We say this is the default modifier.
133+
theorem, and then the hypotheses from left to right. We say this is the default modifier.
134134
Each time it encounters a subexpression which covers an argument which was not
135135
previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
136136
If `grind!` is used, then only minimal indexable subexpressions are considered.

0 commit comments

Comments
 (0)