fact: Fixpoint filter (f:key->elt->bool) m := match m with | Leaf _ => Leaf _ | Node _ l x e r => let l' := filter f l in let r' := filter f r in if f x e then join l' x e r' else concat l' r' end.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)