Ignore:
Timestamp:
Apr 15, 2013, 4:31:50 PM (7 years ago)
Author:
tranquil
Message:
  • removed sigma types from traces of intensional events
  • completed correctness.ma using axiom files, a single daemon remains
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCostsSplit.ma

    r2999 r3145  
    320320  λp.
    321321  let cost_map ≝ compute_costs p in
    322   λl_sig.
    323   lookup_present … cost_map (as_cost_get_label ? l_sig) ?.
    324   cases cost_map #m * #prf #_ cases l_sig
    325   #l * #pc #Hl whd in Hl; whd whd in match (as_cost_get_label ??);
    326   whd in Hl:(??%?); lapply (prf … Hl) //
    327 qed.
     322  λl.
     323  lookup_def … cost_map l 0.
Note: See TracChangeset for help on using the changeset viewer.