Changeset 1573 for src/ASM/Interpret.ma
- Timestamp:
- Nov 28, 2011, 5:13:04 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Interpret.ma
r1547 r1573 785 785 786 786 definition current_instruction_cost ≝ 787 λs: Status. \snd (fetch (code_memory … s) (program_counter … s)). 787 λs: Status. 788 \snd (fetch (code_memory … s) (program_counter … s)). 788 789 789 790 definition execute_1: ∀s:Status. Σs':Status. clock … s' - clock … s = current_instruction_cost s ≝
Note: See TracChangeset
for help on using the changeset viewer.