Changeset 1923


Ignore:
Timestamp:
May 8, 2012, 3:43:37 PM (7 years ago)
Author:
mulligan
Message:

Small change, closing daemon that went under the RADAR

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1921 r1923  
    675675  |8:
    676676    #end_flag #start_status #end_status #trace_any_label #costed_assm
    677     #unrepeating_witness
     677    #unrepeating_witness'
    678678    whd in ⊢ (??%?); whd in ⊢ (??(?%?)?);
    679679    >(compute_trace_any_label_using_paid_ok_with_trace … good_program_witness … cost_map … codom_dom … dom_codom)
     
    687687        generalize in match (tech_cost_of_label0 ? ? ? ? ? ?);
    688688        normalize in match (nth_safe ? ? ? ?);
    689         whd in costed_assm; lapply costed_assm -costed_assm   
     689        whd in costed_assm; lapply costed_assm
    690690        inversion (lookup_opt ? ? (program_counter … cm start_status) cost_labels)
    691691        [1:
     
    698698          #cost -block_cost_assm #block_cost_assm
    699699          cases (block_cost_assm ??? trace_any_label ???)
    700           try @refl
    701           [1:
    702             assumption
    703           |2:
    704             (* XXX: !!! *)
    705             cases daemon
    706           ]
     700          try @refl assumption
    707701        ]
    708702      ]
Note: See TracChangeset for help on using the changeset viewer.