fact: Definition tagOf (d:data) : tag := match d with | ensuresC _ _ => ensuresT | signalsC _ _ => signalsT | signalsOnlyC _ _ => signalsOnlyT | divergesC _ _ => divergesT | whenC _ _ => whenT | assignableC _ _ => assignableT | accessibleC _ _ => accessibleT | callableC _ _ => callableT | measuredByC _ _ => measuredByT | capturesC _ _ => capturesT | workingSpaceC _ _ => workingSpaceT | durationC _ _ => durationT end.
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)