source: Deliverables/D4.1/Matita/DoTest.ma @ 355

Last change on this file since 355 was 355, checked in by sacerdot, 10 years ago

...

File size: 655 bytes
Line 
1include "Test.ma".
2include "Interpret.ma".
3
4ndefinition testmem ≝ assembly test.
5ndefinition teststatus ≝ load testmem initialise_status.
6ndefinition testfinal ≝ execute one teststatus.
7
8notation "'STATUS'" with precedence 90 for @{ 'status }.
9interpretation "status" 'status = (mk_Status ??????????).
10
11(*
12nlemma xoo: testfinal = testfinal.
13 nnormalize in ⊢ (??%?); @;
14nqed.
15*)
16
17nlemma xoo:
18 fetch (code_mem testfinal) (program_counter testfinal) =
19 fetch (code_mem testfinal) (program_counter testfinal).
20 nnormalize in ⊢ (??%?); @;
21nqed.
22
23
24nlemma xoo: program_counter testfinal = program_counter testfinal.
25 nnormalize in ⊢ (??%?); @;
26nqed.
Note: See TracBrowser for help on using the repository browser.