max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/data/rbmap/basic): add RBMap.empty

Browse source
This commit is contained in:
Leonardo de Moura 2019-04-23 09:14:54 -07:00
parent cac080f504
commit 7c0f3aef5b
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
library/init/data/rbmap/basic.lean
View file

@ -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}