Ignore:
Timestamp:
Mar 6, 2013, 12:09:52 PM (8 years ago)
Author:
piccolo
Message:

modified joint_closed_internal_function definition (added condition on pseudo-registers)
added new record for parameters
modified state definition with option for framesT

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semanticsUtils.ma

    r2708 r2783  
    5050}.
    5151
    52 definition reg_store ≝ λreg,v,locals. update RegisterTag beval locals reg v.
     52definition reg_store ≝ λreg,v,locals. OK ? (add RegisterTag beval locals reg v).
    5353
    5454definition reg_retrieve : register_env beval → register → res beval ≝
     
    6969
    7070record sem_graph_params : Type[1] ≝
    71 { sgp_pars : unserialized_params
     71{ sgp_pars : uns_params
    7272; sgp_sup : ∀F.sem_unserialized_params sgp_pars F
    7373}.
     74
    7475
    7576definition sem_graph_params_to_graph_params :
     
    107108
    108109record sem_lin_params : Type[1] ≝
    109 { slp_pars : unserialized_params
     110{ slp_pars : uns_params
    110111; slp_sup : ∀F.sem_unserialized_params slp_pars F
    111112}.
Note: See TracChangeset for help on using the changeset viewer.