Skip to content

Commit 113c835

Browse files
committed
fixes
1 parent 9ce3a59 commit 113c835

File tree

2 files changed

+2
-2
lines changed

2 files changed

+2
-2
lines changed

src/Std/Data/HashMap/Basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -66,7 +66,7 @@ structure HashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] where
6666

6767
namespace HashMap
6868

69-
@[inline, inherit_doc DHashMap.empty] def emptyWithCapacity [BEq α] [Hashable α] (capacity := 8) :
69+
@[inline, inherit_doc DHashMap.emptyWithCapacity] def emptyWithCapacity [BEq α] [Hashable α] (capacity := 8) :
7070
HashMap α β :=
7171
⟨DHashMap.emptyWithCapacity capacity⟩
7272

src/Std/Data/HashMap/Raw.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -64,7 +64,7 @@ structure Raw (α : Type u) (β : Type v) where
6464

6565
namespace Raw
6666

67-
@[inline, inherit_doc DHashMap.Raw.empty] def emptyWithCapacity (capacity := 8) : Raw α β :=
67+
@[inline, inherit_doc DHashMap.Raw.emptyWithCapacity] def emptyWithCapacity (capacity := 8) : Raw α β :=
6868
⟨DHashMap.Raw.emptyWithCapacity capacity⟩
6969

7070
@[deprecated emptyWithCapacity (since := "2025-03-12"), inherit_doc emptyWithCapacity]

0 commit comments

Comments
 (0)