Changeset 1658 for src/common
- Timestamp:
- Jan 25, 2012, 6:18:04 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/StructuredTraces.ma
r1654 r1658 1 1 include "basics/types.ma". 2 2 include "basics/bool.ma". 3 include "basics/jmeq.ma". 3 4 4 5 inductive status_class : Type[0] ≝ … … 95 96 trace_any_label S end_flag status_pre status_end. 96 97 97 98 98 coinductive trace_label_diverges (S:abstract_status) : S → Type[0] ≝ 99 99 | tld_step:
Note: See TracChangeset
for help on using the changeset viewer.