Changeset 928 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Jun 9, 2011, 6:07:29 PM (9 years ago)
Author:
sacerdot
Message:

Technical splitting.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r910 r928  
    513513qed.
    514514
    515 definition execute_1: Status → Status ≝
    516   λs: Status.
    517     let 〈instr_pc, ticks〉 ≝ fetch (code_memory ? s) (program_counter ? s) in
     515definition execute_1_0: Status → instruction × Word × nat → Status ≝
     516  λs,instr_pc_ticks.
     517    let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in
    518518    let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
    519519    let s ≝ set_clock ? s (clock ? s + ticks) in
     
    625625qed.
    626626
     627definition execute_1: Status → Status ≝
     628  λs: Status.
     629    let instr_pc_ticks ≝ fetch (code_memory ? s) (program_counter ? s) in
     630     execute_1_0 s instr_pc_ticks.
     631
    627632let rec index_of_internal (A: Type[0]) (pred: A → bool) (l: list A) (acc: nat) on l: nat ≝
    628633  match l with
Note: See TracChangeset for help on using the changeset viewer.