 Timestamp:
 Mar 8, 2013, 12:26:06 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLToERTLptr.ma
r2818 r2820 75 75 definition translate_data : 76 76 ∀globals.joint_closed_internal_function ERTL globals → 77 bound_b_graph_translate_data ERTL ERTLptr globals≝78 λglobals,def.bret … .79 [try @(mk_b_graph_translate_data …77 bind_new register (b_graph_translate_data ERTL ERTLptr globals) ≝ 78 λglobals,def.bret … 79 (mk_b_graph_translate_data … 80 80 (* init_ret ≝ *) (joint_if_result … def) 81 81 (* init_params ≝ *) (joint_if_params … def) … … 85 85 (* f_step ≝ *) (translate_step globals) 86 86 (* f_fin ≝ *) (translate_fin_step globals) 87 ????) 88  cases daemon ] 89 @hide_prf cases daemon (* 87 ????). 88 @hide_prf 90 89 [ #l * [ #c'  * #f #args #dest  #a #ltrue  #s ] #c whd 91 90 [3: #r1 ] #l' #EQ destruct try % … … 109 108 [ #X #l1 #l2 #EQ destruct elim l2 [ % ] #hd #tl #IH % [ %1 % ] @(All_mp … IH) #x #H %2{H} ] 110 109 #aux @aux cases s // 111 ] *)110 ] 112 111 qed. 113 112 114 113 definition ertl_to_ertlptr: ertl_program → ertlptr_program ≝ 115 114 b_graph_transform_program ERTL ERTLptr translate_data. 115 % 116 qed.
Note: See TracChangeset
for help on using the changeset viewer.