Changeset 844


Ignore:
Timestamp:
May 25, 2011, 4:26:17 PM (8 years ago)
Author:
sacerdot
Message:

Useless code removed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r842 r844  
    645645  λp.
    646646    let 〈preamble, instr_list〉 ≝ p in
    647     match build_maps p with
    648     [ None ⇒ None ?
    649     | Some maps ⇒
    650       let labels ≝ \fst maps in
    651       let datalabels ≝ construct_datalabels preamble in
    652647      match build_maps p with
    653648      [ None ⇒ None ?
    654649      | Some labels_costs ⇒
     650        let datalabels ≝ construct_datalabels preamble in
    655651        let 〈labels,costs〉 ≝ labels_costs in
    656652        let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in
     
    675671          | Some result ⇒ Some ? (〈\snd result, costs〉)
    676672          ]
    677       ]
    678     ].
     673      ].
    679674
    680675definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
Note: See TracChangeset for help on using the changeset viewer.