Ignore:
Timestamp:
Feb 18, 2013, 6:26:22 PM (7 years ago)
Author:
tranquil
Message:
  • a generic graph program transformation
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semanticsUtils.ma

    r2674 r2675  
    33include "utilities/hide.ma".
    44include "ASM/BitVectorTrie.ma".
    5 include "joint/TranslateUtils.ma".
    65
    76record hw_register_env : Type[0] ≝
     
    163162whd in ⊢ (??%%→?); #EQ destruct(EQ) %{EQ1 EQ2}
    164163qed.
    165 
    166 (*lemma b_graph_translate_eval :
    167   ∀src : sem_graph_params.
    168   ∀dst : sem_graph_params.
    169   ∀globals: list ident.
    170   ∀init_ret,init_params,init_stack_size.
    171   ∀f_step,f_fin,def_in.
    172   let def_out ≝
    173     b_graph_translate src_g_pars dst_g_pars globals
    174       init_ret init_params init_stack_size f_step f_fin def_in in
    175   ∀st : state_pc src
    176 *)
Note: See TracChangeset for help on using the changeset viewer.