Ignore:
Timestamp:
Dec 15, 2010, 11:35:37 PM (10 years ago)
Author:
sacerdot
Message:
  1. new function assembly_unlabelled_program
  2. the new function is now used in DoTest?.ma
File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Assembly.ma

    r431 r437  
    431431nqed.
    432432
    433 ndefinition assembly0: assembly_program → Maybe (List Byte × (BitVectorTrie String sixteen)) ≝
     433ndefinition assembly: assembly_program → Maybe (List Byte × (BitVectorTrie String sixteen)) ≝
    434434  λp.
    435435    let 〈preamble, instr_list〉 ≝ p in
     
    518518nqed.
    519519
    520 ndefinition assembly: assembly_program → Maybe (List Byte × (BitVectorTrie String sixteen)) ≝
    521  λp: assembly_program.
    522   Just ? (〈fold_right ?? (λi,l.
    523    match i with [ Instruction i ⇒ assembly1 i @ l | _ ⇒ l] ) [ ] (second ?? p), Stub …〉).
     520ndefinition assembly_unlabelled_program: List instruction → Maybe (List Byte × (BitVectorTrie String sixteen)) ≝
     521 λp.Just ? (〈fold_right ?? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
Note: See TracChangeset for help on using the changeset viewer.