Changeset 3021 for src/Clight/label.ma


Ignore:
Timestamp:
Mar 28, 2013, 7:11:09 PM (8 years ago)
Author:
campbell
Message:

Replace clight_clock_after with a more sensible definition that uses
an intensional trace. Also drop the proof argument for the clight cost
map to avoid proving that costs come from the clight program - it doesn't
seem to give us much of a benefit.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/label.ma

    r2588 r3021  
    5656  λp. Σl. in_clight_program p l.
    5757
     58(* Providing these proofs isn't easy, and doesn't seem to have any benefit, so
     59   let's stick with a simpler form.
    5860definition clight_cost_map ≝
    5961  λp. (in_clight_label p) → ℕ.
     62*)
     63
     64definition clight_cost_map ≝ costlabel → ℕ.
    6065
    6166definition clight_label_free : clight_program → bool ≝
Note: See TracChangeset for help on using the changeset viewer.