Changeset 2001 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
May 25, 2012, 1:47:32 PM (8 years ago)
Author:
campbell
Message:

Get the compiler to output more.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1976 r2001  
    722722  @nat_of_bitvector_lt_bound
    723723qed.
    724 
    725 definition ASM_cost_map :
    726   ∀code_memory: BitVectorTrie Byte 16.
    727   ∀cost_labels: BitVectorTrie costlabel 16.
    728   ∀cost_map: identifier_map CostTag nat.
    729   (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k) →
    730   as_cost_map (ASM_abstract_status code_memory cost_labels) ≝
    731   λcode_memory,cost_labels,cost_map,codom_dom,l_sig.
    732   (lookup_present … cost_map (pi1 … l_sig) ?).
    733   cases l_sig #l * #pc @(codom_dom pc)
    734   qed.
    735724 
    736725include "utilities/permutations.ma".
Note: See TracChangeset for help on using the changeset viewer.