Ignore:
Timestamp:
Mar 15, 2013, 12:16:30 PM (7 years ago)
Author:
tranquil
Message:

changed coercion from list of joint_seq to blocks to a more efficient one

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics_blocks.ma

    r2869 r2879  
    22include "joint/Traces.ma".
    33include "joint/semanticsUtils.ma".
    4 
    5 include "common/StatusSimulation.ma". (* for trace_any_any_free *)
    64
    75(* let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝
     
    1412  λp : evaluation_params.λcurr_id.
    1513  m_fold … (eval_seq_no_pc … (ev_genv … p) curr_id).
     14
     15lemma repeat_eval_seq_no_pc_append :
     16  ∀p,curr_id,L1,L2,s.
     17  repeat_eval_seq_no_pc p curr_id (L1@L2) s =
     18  ! s' ← repeat_eval_seq_no_pc p curr_id L1 s;
     19  repeat_eval_seq_no_pc p curr_id L2 s' ≝
     20  λp,curr_id.m_fold_append ….
    1621
    1722lemma produce_step_trace :
Note: See TracChangeset for help on using the changeset viewer.