Changeset 781 for src/common


Ignore:
Timestamp:
Apr 28, 2011, 4:43:50 PM (9 years ago)
Author:
campbell
Message:

Implement labelling pass for Clight.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Events.ma

    r720 r781  
    7070  ].
    7171
     72(* Useful for testing programs. *)
     73definition remove_costs : trace → trace ≝
     74filter … (λe. match e with [ EVcost _ ⇒ false | _ ⇒ true ]).
     75
    7276(* * Concatenation of traces is written [**] in the finite case
    7377  or [***] in the infinite case. *)
Note: See TracChangeset for help on using the changeset viewer.