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

Last change on this file since 446 was 439, checked in by mulligan, 10 years ago

Changes to get everything to compile.

File size: 514 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 eight two_hundred_and_fifty_six)
13               (bitvector_of_nat eight one) false =
14  sub_8_with_carry (bitvector_of_nat eight two_hundred_and_fifty_six)
15               (bitvector_of_nat eight one) false.
16  nnormalize;
17  @;
18nqed.
Note: See TracBrowser for help on using the repository browser.