chore(library/init/data/rbmap/basic): use [specialize] instead of [inline]

`RBMap.insert` is not that small.
This commit is contained in:
Leonardo de Moura 2019-05-03 21:09:07 -07:00
parent b6c4caf725
commit 626e8fb27f

View file

@ -100,7 +100,7 @@ def setBlack : RBNode α β → RBNode α β
| (node _ l k v r) := node black l k v r
| e := e
@[inline] def insert (t : RBNode α β) (k : α) (v : β k) : RBNode α β :=
@[specialize] def insert (t : RBNode α β) (k : α) (v : β k) : RBNode α β :=
if isRed t then setBlack (ins lt t k v)
else ins lt t k v