Changeset 3003


Ignore:
Timestamp:
Mar 28, 2013, 1:08:51 PM (4 years ago)
Author:
sacerdot
Message:

Correctness.ma "repaired"

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/correctness.ma

    r2999 r3003  
    9393include "common/AssocList.ma".
    9494
    95 definition lookup_stack_cost : stack_cost_model → ident → nat ≝
     95definition lookup_stack_cost : stack_cost_model → ident → option nat ≝
    9696 λstack_cost,id.
    97   match assoc_list_lookup ?? id (eq_identifier …) stack_cost with
    98   [ None ⇒ 0 | Some n ⇒ n ].
     97  assoc_list_lookup ?? id (eq_identifier …) stack_cost.
    9998
    10099definition simulates ≝
    101100  λp: compiler_output.
    102   let initial_status ≝ initialise_status … (cm c_labelled_object_code … p) in
     101  let initial_status ≝ initialise_status … (cm (c_labelled_object_code … p)) in
    103102  ∀m1,m2.
    104103   measurable Clight_pcs (c_labelled_clight … p) m1 m2
Note: See TracChangeset for help on using the changeset viewer.