Changeset 2288 for src/RTLabs/CostSpec.ma
- Timestamp:
- Aug 2, 2012, 5:04:36 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/CostSpec.ma
r2226 r2288 22 22 is_cost_label (lookup_present … (f_graph f) l1 ?) = true ∧ 23 23 is_cost_label (lookup_present … (f_graph f) l2 ?) = true 24 | St_jumptable _ ls ⇒ λH.24 (*| St_jumptable _ ls ⇒ λH. 25 25 (* I did have a dependent version of All here, but it's a pain. *) 26 All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls 26 All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls*) 27 27 | _ ⇒ λ_. True 28 28 ]. whd in H; … … 55 55 *) 56 56 | St_cond _ l1 l2 ⇒ [l1; l2] 57 | St_jumptable _ ls ⇒ ls 57 (*| St_jumptable _ ls ⇒ ls*) 58 58 | St_return ⇒ [ ] 59 59 ].
Note: See TracChangeset
for help on using the changeset viewer.