Changeset 722 for src/ASM


Ignore:
Timestamp:
Mar 29, 2011, 6:32:47 PM (10 years ago)
Author:
mulligan
Message:

Committing changes from today. Several files do not typecheck.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r714 r722  
    185185definition instruction ≝ preinstruction [[relative]].
    186186
    187 inductive labelled_instruction: Type[0] ≝
    188   Instruction: instruction → labelled_instruction
    189 | Cost: Identifier → labelled_instruction
    190 | Jmp: Identifier → labelled_instruction
    191 | Call: Identifier → labelled_instruction
    192 | Mov: [[dptr]] → Identifier → labelled_instruction
    193 | Label: Identifier → labelled_instruction
    194 | WithLabel: jump Identifier → labelled_instruction.
     187inductive pseudo_instruction: Type[0] ≝
     188  Instruction: instruction → pseudo_instruction
     189| Comment: String → pseudo_instruction
     190| Cost: Identifier → pseudo_instruction
     191| Jmp: Identifier → pseudo_instruction
     192| Call: Identifier → pseudo_instruction
     193| Mov: [[dptr]] → Identifier → pseudo_instruction
     194| WithLabel: jump Identifier → pseudo_instruction.
     195
     196definition labelled_instruction ≝ option Identifier × pseudo_instruction.
    195197
    196198definition preamble ≝ list (Identifier × nat).
Note: See TracChangeset for help on using the changeset viewer.