source: src/ASM/Debug.ma @ 688

Last change on this file since 688 was 472, checked in by mulligan, 10 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.