Changeset 1573 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Nov 28, 2011, 5:13:04 PM (8 years ago)
Author:
mulligan
Message:

more complicated than it appears :(

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/Interpret.ma

    r1547 r1573  
    785785
    786786definition 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)).
    788789
    789790definition execute_1: ∀s:Status. Σs':Status. clock … s' - clock … s = current_instruction_cost s ≝
Note: See TracChangeset for help on using the changeset viewer.