Ignore:
Timestamp:
Aug 2, 2012, 5:04:36 PM (8 years ago)
Author:
campbell
Message:

Remove jumptables from RTLabs. :(

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/CostSpec.ma

    r2226 r2288  
    2222    is_cost_label (lookup_present … (f_graph f) l1 ?) = true ∧
    2323    is_cost_label (lookup_present … (f_graph f) l2 ?) = true
    24 | St_jumptable _ ls ⇒ λH.
     24(*| St_jumptable _ ls ⇒ λH.
    2525    (* 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*)
    2727| _ ⇒ λ_. True
    2828]. whd in H;
     
    5555*)
    5656| St_cond _ l1 l2 ⇒ [l1; l2]
    57 | St_jumptable _ ls ⇒ ls
     57(*| St_jumptable _ ls ⇒ ls*)
    5858| St_return ⇒ [ ]
    5959].
Note: See TracChangeset for help on using the changeset viewer.