Ignore:
Timestamp:
Dec 1, 2010, 11:27:04 PM (9 years ago)
Author:
sacerdot
Message:
  • stupid bug fixed in BitVectorTrie?
  • dependencies minimized, dead code removed
File:
1 edited

Legend:

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

    r355 r357  
    1515*)
    1616
     17(*
     18nlemma test:
     19 (let status ≝
     20 load
     21  (assembly [LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;true;false;false;false]])])
     22   initialise_status
     23  in
     24   fetch (code_memory status) (program_counter status)
     25  ) = ?.
     26##[ nnormalize in ⊢ (??%?);
     27*)
     28
     29
    1730nlemma xoo:
    18  fetch (code_mem testfinal) (program_counter testfinal) =
    19  fetch (code_mem testfinal) (program_counter testfinal).
     31 fetch (code_memory testfinal) (program_counter testfinal) =
     32 fetch (code_memory testfinal) (program_counter testfinal).
    2033 nnormalize in ⊢ (??%?); @;
    2134nqed.
    22 
     35*)
    2336
    2437nlemma xoo: program_counter testfinal = program_counter testfinal.
Note: See TracChangeset for help on using the changeset viewer.