fact: Definition mapType (t:tag) : Type := match t with | ensuresT => optional Expression | signalsT => (Param * optional Expression) | signalsOnlyT => list StaticType | divergesT => optional Expression | whenT => optional Expression | assignableT => optional StoreRefList | accessibleT => optional StoreRefList | callableT => optional CallableList | measuredByT => (optional Expression * option Expression) | capturesT => optional StoreRefList | workingSpaceT => (optional Expression * option Expression) | durationT => (optional Expression * option Expression) end.
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)