max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: trivial typo in Grind/Attr.lean (#11676)

Browse source 
This PR fixes typo "the the custom pattern" -> "the custom pattern".
This commit is contained in:
Evan Chen 2025-12-14 12:12:47 -08:00 • committed by GitHub
parent c4d67c22e6
commit 429e09cd82
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Grind/Attr.lean
View file

@ -143,7 +143,7 @@ the `grind_pattern` command, which lets you specify how `grind` should
match and use particular theorems.
Example:
- `grind [usr myThm]` means `grind` is using `myThm`, but with the
- `grind [usr myThm]` means `grind` is using `myThm`, but with
the custom pattern you defined with `grind_pattern`.
-/
syntax grindUsr := &"usr"