Changeset 2757 for src/common


Ignore:
Timestamp:
Mar 1, 2013, 7:13:49 PM (7 years ago)
Author:
tranquil
Message:

many things are still broken, but there is a partial backtrack on Structured traces's execute

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r2756 r2757  
    1717record abstract_status : Type[1] ≝
    1818  { as_status :> Type[0]
    19   ; as_eval : as_status → IO io_out io_in as_status
    20   ; as_init : res as_status
     19  ; as_execute : relation as_status
    2120  ; as_pc : DeqSet
    2221  ; as_pc_of : as_status → as_pc
     
    3231definition as_call ≝ λS,s,f.as_call_ident S s = f.
    3332definition as_final ≝ λS,s.as_result S s ≠ None ?.
    34 definition as_execute ≝ λS,s1,s2.as_eval S s1 = Value … s2.
    3533
    3634definition as_label ≝ λS : abstract_status. λs : S. as_label_of_pc ? (as_pc_of ? s).
Note: See TracChangeset for help on using the changeset viewer.