- Timestamp:
- Jun 9, 2011, 6:07:29 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Interpret.ma
r910 r928 513 513 qed. 514 514 515 definition execute_1 : Status→ Status ≝516 λs : Status.517 let 〈instr_pc, ticks〉 ≝ fetch (code_memory ? s) (program_counter ? s)in515 definition execute_1_0: Status → instruction × Word × nat → Status ≝ 516 λs,instr_pc_ticks. 517 let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in 518 518 let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in 519 519 let s ≝ set_clock ? s (clock ? s + ticks) in … … 625 625 qed. 626 626 627 definition 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 627 632 let rec index_of_internal (A: Type[0]) (pred: A → bool) (l: list A) (acc: nat) on l: nat ≝ 628 633 match l with
Note: See TracChangeset
for help on using the changeset viewer.