fact: Definition extractClauses (t:TAG.tag) (redundant:bool) (l:list TAG.data) : list (TAG.mapType t) := let lFiltered1 := TAG.filterTag t l in let lFiltered2 := TAG.filterTagData t (fun c => eqb (methodSpecClauseRedundant c) redundant) lFiltered1 in TAG.mapData2Type t lFiltered2.
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)