Changeset 2950


Ignore:
Timestamp:
Mar 25, 2013, 10:39:07 PM (4 years ago)
Author:
sacerdot
Message:

linearise repaired (did I do the right thing???)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/linearise.ma

    r2946 r2950  
    881881
    882882definition 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)) ℕ*)
    885887   ≝
    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
    888895      (λglobals.transf_fundef ?? (λf_in.\fst (linearise_int_fun p globals f_in)))
    889896      (init_cost_label … pr).
    890 
     897*)
    891898(*
    892899definition good_sigma :
Note: See TracChangeset for help on using the changeset viewer.