fact: Fixpoint weaklyImplementsList (l:list Implements) : list Interface := match l with | (implements _)::xs => (weaklyImplementsList xs) | (implements_weakly i)::xs => i :: (weaklyImplementsList xs) | nil => nil end.
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)