fact: Definition mkBasicClause : forall t:tag, mapType t -> basicClauseType t := fun t0 cl => match t0 as x return (t0 = x -> basicClauseType x) with | ensuresT => fun Heq => ENSURES.Build_t (let H := eq_rect t0 (fun t1 : tag => mapType t1) cl ensuresT Heq in H) | signalsT => fun Heq => SIGNALS.Build_t (let H := eq_rect t0 (fun t1 : tag => mapType t1) cl signalsT Heq in snd H) | signalsOnlyT => fun Heq => SIGNALS_ONLY.Build_t (let H := eq_rect t0 (fun t1 : tag => mapType t1) cl signalsOnlyT Heq in H) | divergesT => fun Heq => DIVERGES.Build_t (let H := eq_rect t0 (fun t1 : tag => mapType t1) cl divergesT Heq in H) | whenT => fun Heq => WHEN.Build_t (let H := eq_rect t0 (fun t1 : tag => mapType t1) cl whenT Heq in H) | assignableT => fun Heq => ASSIGNABLE.Build_t (let H := eq_rect t0 (fun t1 : tag => mapType t1) cl assignableT Heq in H) | accessibleT => fun Heq => ACCESSIBLE.Build_t (let H := eq_rect t0 (fun t1 : tag => mapType t1) cl accessibleT Heq in H) | callableT => fun Heq => CALLABLE.Build_t (let H := eq_rect t0 (fun t1 : tag => mapType t1) cl callableT Heq in H) | measuredByT => fun Heq => MEASURED_BY.Build_t (let H := eq_rect t0 (fun t1 : tag => mapType t1) cl measuredByT Heq in fst H) (let H := eq_rect t0 (fun t1 : tag => mapType t1) cl measuredByT Heq in snd H) | capturesT => fun Heq => CAPTURES.Build_t (let H := eq_rect t0 (fun t1 : tag => mapType t1) cl capturesT Heq in H) | workingSpaceT => fun Heq => WORKING_SPACE.Build_t (let H := eq_rect t0 (fun t1 : tag => mapType t1) cl workingSpaceT Heq in fst H) (let H := eq_rect t0 (fun t1 : tag => mapType t1) cl workingSpaceT Heq in snd H) | durationT => fun Heq => DURATION.Build_t (let H := eq_rect t0 (fun t1 : tag => mapType t1) cl durationT Heq in fst H) (let H := eq_rect t0 (fun t1 : tag => mapType t1) cl durationT Heq in snd H) end (refl_equal t0).
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)