fact: Definition MatchCombineSearchTerm {heading} {SearchTerm1 SearchTerm2} (Matcher1 : SearchTerm1 -> @RawTuple heading -> bool) (Matcher2 : SearchTerm2 -> @RawTuple heading -> bool) (st : CombineSearchTerm SearchTerm1 SearchTerm2) (tup : @RawTuple heading) : bool := match st with | (Some st1, Some st2) => Matcher1 st1 tup && Matcher2 st2 tup | (None, Some st2) => Matcher2 st2 tup | (Some st1, None) => Matcher1 st1 tup | _ => true end.
imports: Coq.Lists.List Coq.Program.Program Coq.Bool.Bool Coq.Strings.String Coq.Structures.OrderedTypeEx Coq.Arith.Arith Fiat.Common.ilist3 Fiat.Common.i3list Fiat.Common.Ensembles.IndexedEnsembles Fiat.Computation Fiat.ADT Fiat.ADTRefinement Fiat.ADTNotation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Representation.QueryStructure Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.Common.ilist3_pair Fiat.Common.ilist3 Fiat.Common.i3list2 Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsOfTuples Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagImplementation