source: Deliverables/D4.1/Matita/Debug.ma @ 475

Last change on this file since 475 was 472, checked in by mulligan, 9 years ago

More changes to debug and testing files to get them to work with the standard library.

File size: 450 bytes
Line 
1include "Status.ma".
2include "Interpret.ma".
3
4nlemma test1:
5  bit_address_of_register (initialise_status) [[ false; false; false ]] =
6  bit_address_of_register (initialise_status) [[ false; false; false ]].
7  nnormalize;
8  @;
9nqed.
10
11nlemma test2:
12  sub_8_with_carry (bitvector_of_nat 8 256)
13               (bitvector_of_nat 8 1) false =
14  sub_8_with_carry (bitvector_of_nat 8 256)
15               (bitvector_of_nat 8 1) false.
16  nnormalize;
17  @;
18nqed.
Note: See TracBrowser for help on using the repository browser.