Changeset 2226 for src/RTLabs/CostSpec.ma
- Timestamp:
- Jul 20, 2012, 6:36:34 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/CostSpec.ma
r2218 r2226 76 76 77 77 definition well_cost_labelled_program : RTLabs_program → Prop ≝ 78 λp. All ? (λx. let 〈id,fd〉 ≝ x in 79 match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | _ ⇒ True]) (prog_funct … p). 78 λp. All ? (λx. match \snd x with [ Internal fn ⇒ 79 well_cost_labelled_fn fn ∧ soundly_labelled_fn fn 80 | _ ⇒ True]) (prog_funct … p). 80 81 81 82
Note: See TracChangeset
for help on using the changeset viewer.