Changeset 1597 for src/ASM/Fetch.ma
- Timestamp:
- Dec 12, 2011, 9:51:21 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Fetch.ma
r1591 r1597 42 42 definition fetch0: BitVectorTrie Byte 16 → ∀program_counter: Word. Byte → 43 43 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)) ≝ 45 45 λpmem. 46 46 λpc. … … 425 425 426 426 definition 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)) ≝ 428 428 λpmem: BitVectorTrie Byte 16. 429 429 λpc: Word.
Note: See TracChangeset
for help on using the changeset viewer.