Changeset 2475 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
Nov 19, 2012, 5:13:21 PM (7 years ago)
Author:
campbell
Message:

Get compiler.ma and correctness.ma checking again. Note that the back-end
is in a state of flux at the moment, so is axiomatised out.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1964 r2475  
    1313      word_deqset
    1414      (program_counter …)
    15       (λs,class. ASM_classify … s = class)
     15      (λs. ASM_classify … s)
    1616      (λpc.lookup_opt ?? pc cost_labels)
    1717      (next_instruction_properly_relates_program_counters code_memory)
     18      ?
    1819      ?.
    19   cases daemon (* XXX: is final predicate *)
     20  cases daemon (* XXX: is final predicate, call ident function *)
    2021qed.
    2122
Note: See TracChangeset for help on using the changeset viewer.