Changeset 2123 for src/ASM/Status.ma


Ignore:
Timestamp:
Jun 27, 2012, 4:04:14 PM (8 years ago)
Author:
boender
Message:
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Status.ma

    r2119 r2123  
    11451145qed.
    11461146
     1147definition is_well_labelled_p ≝
     1148  λinstr_list.
     1149  ∀id: Identifier.
     1150  ∀ppc. ∀ppc_ok.
     1151  ∀i.
     1152    fetch_pseudo_instruction instr_list ppc ppc_ok = i →
     1153      instruction_has_label id (\fst i) →
     1154        occurs_exactly_once ASMTag pseudo_instruction id instr_list.
     1155
    11471156definition address_of_word_labels_code_mem ≝
    11481157  λcode_mem : list labelled_instruction.
Note: See TracChangeset for help on using the changeset viewer.