Ignore:
Timestamp:
Feb 12, 2013, 2:41:22 AM (7 years ago)
Author:
sacerdot
Message:

Cost proof fully repaired. It was broken by the definitions used in compiler.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCostsSplit.ma

    r2516 r2657  
    327327      traverse_code code_memory cost_labels cost_labels_injective.
    328328
    329 (* use of this defn in ASM/CostsProof.ma is ill-typed *)
    330329definition ASM_cost_map :
    331330  ∀p: (list Byte) × (BitVectorTrie costlabel 16).
Note: See TracChangeset for help on using the changeset viewer.