Changeset 2774 for src/joint/Joint.ma
 Timestamp:
 Mar 5, 2013, 6:15:06 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/Joint.ma
r2712 r2774 530 530 definition joint_program ≝ 531 531 λp:params. program (joint_function p) nat. 532 533 (* The cost model for stack consumption *) 534 definition stack_cost_model ≝ list (ident × nat). 535 536 definition stack_cost : ∀p:params. joint_program p → stack_cost_model ≝ 537 λp,pr. 538 foldr … 539 (λid_fun,acc. let 〈id,fun〉 ≝ id_fun in 540 match fun with 541 [ Internal jif ⇒ 〈id,joint_if_stacksize ?? (pi1 … jif)〉::acc 542  External _ ⇒ acc ]) 543 [ ] (prog_funct ?? pr). 544
Note: See TracChangeset
for help on using the changeset viewer.