 Timestamp:
 Mar 25, 2013, 10:39:07 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/linearise.ma
r2946 r2950 881 881 882 882 definition linearise : ∀p : uns_params. 883 program (joint_function (mk_graph_params p)) ℕ → 884 program (joint_function (mk_lin_params p)) ℕ 883 joint_program (mk_graph_params p) → 884 joint_program (mk_lin_params p) 885 (*program (joint_function (mk_graph_params p)) ℕ → 886 program (joint_function (mk_lin_params p)) ℕ*) 885 887 ≝ 886 λp,pr.transform_program ??? pr 887 mk_joint_program 888 λp,pr.(*transform_program ??? pr*) 889 mk_joint_program ? 890 (transform_program ??? pr 891 (λglobals.transf_fundef ?? (λf_in.\fst (linearise_int_fun p globals f_in)))) 892 (init_cost_label ? pr). 893 894 (* mk_joint_program 888 895 (λglobals.transf_fundef ?? (λf_in.\fst (linearise_int_fun p globals f_in))) 889 896 (init_cost_label … pr). 890 897 *) 891 898 (* 892 899 definition good_sigma :
Note: See TracChangeset
for help on using the changeset viewer.