Additional dependent raw tree map operations #
This file defines more operations on Std.DTreeMap.Raw
.
We currently do not provide lemmas for these functions.
@[inline]
def
Std.DTreeMap.Raw.filterMap
{α : Type u}
{β : α → Type v}
{γ : α → Type w}
{cmp : α → α → Ordering}
(f : (a : α) → β a → Option (γ a))
(t : Raw α β cmp)
:
Raw α γ cmp
Updates the values of the map by applying the given function to all mappings, keeping
only those mappings where the function returns some
value.
Equations
Instances For
We do not provide get*GE
, get*GT
, get*LE
and get*LT
functions for the raw trees.