Ignore:
Timestamp:
Nov 24, 2011, 6:49:51 PM (8 years ago)
Author:
campbell
Message:

Add a notion of flat traces with evidence for RTLabs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/semantics.ma

    r1535 r1559  
    197197] qed.
    198198
    199 definition is_final : state → option int ≝
     199definition RTLabs_is_final : state → option int ≝
    200200λs. match s with
    201201[ State _ _ _ ⇒ None ?
     
    212212
    213213definition RTLabs_exec : trans_system io_out io_in ≝
    214   mk_trans_system … ? (λ_.is_final) eval_statement.
     214  mk_trans_system … ? (λ_.RTLabs_is_final) eval_statement.
    215215
    216216definition make_global : RTLabs_program → genv ≝
Note: See TracChangeset for help on using the changeset viewer.