Changeset 1597 for src/ASM/Fetch.ma


Ignore:
Timestamp:
Dec 12, 2011, 9:51:21 AM (9 years ago)
Author:
mulligan
Message:

fixed fetch for jaap

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/Fetch.ma

    r1591 r1597  
    4242definition fetch0: BitVectorTrie Byte 16 → ∀program_counter: Word. Byte →
    4343  nat_of_bitvector … program_counter < code_memory_size - 24 (* 3 bytes *) →
    44   Σret: instruction × Word × nat. nat_of_bitvector … program_counter ≤ nat_of_bitvector … (\snd (\fst ret)) ≝
     44  Σret: instruction × Word × nat. nat_of_bitvector … program_counter < nat_of_bitvector … (\snd (\fst ret)) ≝
    4545  λpmem.
    4646  λpc.
    … …  
    425425
    426426definition fetch: BitVectorTrie Byte 16 → ∀program_counter: Word.
    427     Σret: instruction × Word × nat. nat_of_bitvector … program_counter ≤ nat_of_bitvector … (\snd (\fst ret)) ≝
     427    Σret: instruction × Word × nat. nat_of_bitvector … program_counter < nat_of_bitvector … (\snd (\fst ret)) ≝
    428428  λpmem: BitVectorTrie Byte 16.
    429429  λpc: Word.
Note: See TracChangeset for help on using the changeset viewer.