Changeset 2754 for src/ASM/CodeMemory.ma


Ignore:
Timestamp:
Mar 1, 2013, 10:26:31 AM (7 years ago)
Author:
sacerdot
Message:
  1. WARNING: I commented out one of James's function used in compiler.ma because it was undefined (partial commit). To be restored.
  2. The type of labelled_object_code programs now has a symbol table, used to generate the intensional events function call/return.
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CodeMemory.ma

    r2750 r2754  
    247247(* ***** Object-code ***** JHM: push elsewherein ASM/*.ma? *)
    248248
    249 definition object_code ≝ list Byte.
    250 
    251249inductive nat_bounded : nat → nat → Type[0] ≝
    252250| nat_ok : ∀n,m:nat. nat_bounded n (n+m)
Note: See TracChangeset for help on using the changeset viewer.