From 7c0f3aef5bae67da7952d5d4bd13e3a7a2b0ac75 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 23 Apr 2019 09:14:54 -0700 Subject: [PATCH] feat(library/init/data/rbmap/basic): add `RBMap.empty` --- library/init/data/rbmap/basic.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/library/init/data/rbmap/basic.lean b/library/init/data/rbmap/basic.lean index 96fbbea6de..e0584a5238 100644 --- a/library/init/data/rbmap/basic.lean +++ b/library/init/data/rbmap/basic.lean @@ -148,8 +148,11 @@ def RBMap (α : Type u) (β : Type v) (lt : α → α → Bool) : Type (max u v) @[inline] def mkRBMap (α : Type u) (β : Type v) (lt : α → α → Bool) : RBMap α β lt := ⟨leaf, WellFormed.leafWff lt⟩ +@[inline] def RBMap.empty {α : Type u} {β : Type v} {lt : α → α → Bool} : RBMap α β lt := +mkRBMap _ _ _ + instance (α : Type u) (β : Type v) (lt : α → α → Bool) : HasEmptyc (RBMap α β lt) := -⟨mkRBMap α β lt⟩ +⟨RBMap.empty⟩ namespace RBMap variables {α : Type u} {β : Type v} {σ : Type w} {lt : α → α → Bool}