Skip to content

Commit 155823b

Browse files
committed
doc(Algebra/HierarchyDesign): fix typo in library note (leanprover-community#39149)
Fix instance name (error was possibly caused by the change in the instance naming algorithm).
1 parent 5f02abe commit 155823b

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Mathlib/Algebra/HierarchyDesign.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -232,7 +232,7 @@ Certain instances always apply during type-class resolution. For example, the in
232232
resolution problems of the form `AddGroup _`, and type-class inference will then do an
233233
exhaustive search to find a commutative group. These instances take a long time to fail.
234234
Other instances will only apply if the goal has a certain shape. For example
235-
`Int.instAddGroupInt : AddGroup ℤ` or
235+
`Int.instAddGroup : AddGroup ℤ` or
236236
`Prod.instAddGroup {α β} [AddGroup α] [AddGroup β] : AddGroup (α × β)`. Usually these instances
237237
will fail quickly, and when they apply, they are almost always the desired instance.
238238
For this reason, we want the instances of the second type (that only apply in specific cases) to

0 commit comments

Comments
 (0)