Changeset 1658 for src/common


Ignore:
Timestamp:
Jan 25, 2012, 6:18:04 PM (8 years ago)
Author:
mulligan
Message:

asm costs changes from today

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/common/StructuredTraces.ma

    r1654 r1658  
    11include "basics/types.ma".
    22include "basics/bool.ma".
     3include "basics/jmeq.ma".
    34
    45inductive status_class : Type[0] ≝
    … …  
    9596          trace_any_label S end_flag status_pre status_end.
    9697
    97 
    9898coinductive trace_label_diverges (S:abstract_status) : S → Type[0] ≝
    9999  | tld_step:
Note: See TracChangeset for help on using the changeset viewer.