Skip to content

Commit 22da866

Browse files
committed
doc(Tactic/MinImports): tidy backticks (#31861)
Found and fixed with help from Codex. This is the last remaining true positive finding of the detection script in #31463.
1 parent 5495d7e commit 22da866

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

Mathlib/Tactic/MinImports.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -113,7 +113,7 @@ def getAttrNames (stx : Syntax) : NameSet :=
113113
| some stx => getIds stx
114114

115115
/-- `getAttrs env stx` returns all attribute declaration names contained in `stx` and registered
116-
in the `Environment `env`. -/
116+
in the `Environment` `env`. -/
117117
def getAttrs (env : Environment) (stx : Syntax) : NameSet :=
118118
Id.run do
119119
let mut new : NameSet := {}

0 commit comments

Comments
 (0)