Ignore:
Timestamp:
May 9, 2013, 11:12:07 AM (8 years ago)
Author:
piccolo
Message:

reverted joint_semantics rtl_semantics and ltl_semantics

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/joint_LTL_LIN_semantics.ma

    r3259 r3261  
    11include "LIN/joint_LTL_LIN.ma".
    22include "joint/semanticsUtils.ma".
    3 
     3 
    44definition hw_reg_store ≝ λr,v,e. OK … (hwreg_store r v e).
    55definition hw_reg_retrieve ≝ λl,r. OK … (hwreg_retrieve l r).
     
    8686  (* allocate_local     ≝ *) (λabs.match abs in void with [ ])
    8787*)  (* save_frame         ≝ *) LTL_LIN_save_frame
    88   (* setup_call         ≝ *) (λ_.λ_.λ_.λ_.λ_.λ_.λst.return st)
     88  (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
    8989  (* fetch_external_args≝ *) ltl_lin_fetch_external_args
    9090  (* set_result         ≝ *) ltl_lin_set_result
Note: See TracChangeset for help on using the changeset viewer.