Changeset 3145 for src/ASM/ASMCostsSplit.ma

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:

• src/ASM/ASMCostsSplit.ma (modified) (1 diff)

src/ASM/ASMCostsSplit.ma

@@ -320 +320 @@
   λp.
   let cost_map ≝ compute_costs p in
-  λl_sig.
-  lookup_present … cost_map (as_cost_get_label ? l_sig) ?.
-  cases cost_map #m * #prf #_ cases l_sig
-  #l * #pc #Hl whd in Hl; whd whd in match (as_cost_get_label ??);
-  whd in Hl:(??%?); lapply (prf … Hl) //
-qed.
+  λl.
+  lookup_def … cost_map l 0.