From b4ea61e79d4955a33699db563f933b76b24aecc0 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 22 Sep 2020 14:05:47 +0200 Subject: [PATCH] fix: `NameSet.insert` return type --- src/Lean/Data/Name.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Data/Name.lean b/src/Lean/Data/Name.lean index d84f4c8a0f..eb6ea552d8 100644 --- a/src/Lean/Data/Name.lean +++ b/src/Lean/Data/Name.lean @@ -167,7 +167,7 @@ namespace NameSet def empty : NameSet := mkRBTree Name Name.quickLt instance : HasEmptyc NameSet := ⟨empty⟩ instance : Inhabited NameSet := ⟨{}⟩ -def insert (s : NameSet) (n : Name) := Std.RBTree.insert s n +def insert (s : NameSet) (n : Name) : NameSet := Std.RBTree.insert s n def contains (s : NameSet) (n : Name) : Bool := Std.RBMap.contains s n end NameSet