fact: Definition IBagMatcher (Matcher : TSearchTerm -> TItem -> bool) (imap : TIndex -> option TItem) (searchterm : TSearchTerm) (idx : TIndex) := match imap idx with | None => false | Some item => Matcher searchterm item end.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties