fact: Definition basicClauseType (t:tag) : Type := match t with | ensuresT => ENSURES.t | signalsT => SIGNALS.t | signalsOnlyT => SIGNALS_ONLY.t | divergesT => DIVERGES.t | whenT => WHEN.t | assignableT => ASSIGNABLE.t | accessibleT => ACCESSIBLE.t | callableT => CALLABLE.t | measuredByT => MEASURED_BY.t | capturesT => CAPTURES.t | workingSpaceT => WORKING_SPACE.t | durationT => DURATION.t end.
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)