Changeset 1606 for src/ASM/Interpret2.ma


Ignore:
Timestamp:
Dec 14, 2011, 1:40:08 PM (8 years ago)
Author:
sacerdot
Message:

Porting to last library of Matita.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret2.ma

    r1550 r1606  
    4646 let 〈instr_pc,ticks〉 ≝ fetch (code_memory … s) (program_counter … s) in
    4747 let 〈instr,pc〉 ≝ instr_pc in
    48  let s ≝ eject … (execute_1 s) in
    4948 match lookup_opt … pc costs with
    5049 [ None ⇒ ret … 〈E0, s〉
    51  | Some cst ⇒ ret … 〈Echarge cst, s〉 ].
     50 | Some cst ⇒ ret … 〈Echarge cst, execute_1 s〉 ].
    5251
    5352axiom is_final: BitVectorTrie costlabel 16 → Status → option int.
Note: See TracChangeset for help on using the changeset viewer.