Changeset 2505 for src/Clight/label.ma


Ignore:
Timestamp:
Nov 29, 2012, 3:37:22 PM (8 years ago)
Author:
mckinna
Message:

Cleaned up compiler.ma; some refactoring/additional code needed in Clight/label, and a tweak to translate_cst in RTLabsToRTL to restore its checked status.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/label.ma

    r2399 r2505  
    5353λp,l. Exists … (λx.x=l) (labels_of_clight p).
    5454
     55definition in_clight_label ≝
     56  λp. Σl. in_clight_program p l.
     57
     58definition clight_cost_map ≝
     59  λp. (in_clight_label p) → ℕ.
     60
    5561definition clight_label_free : clight_program → bool ≝
    5662λp. match labels_of_clight p with [ nil ⇒ true | _ ⇒ false ].
Note: See TracChangeset for help on using the changeset viewer.