Ignore:
Timestamp:
Nov 30, 2010, 6:13:00 PM (10 years ago)
Author:
mulligan
Message:

Work on main execution loop. All cases covered. Need to close open proof states and remove computational axioms.

File:
1 edited

Legend:

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

    r346 r347  
    1 (*include "Interpret.ma".*)
     1include "Interpret.ma".
    22include "Assembly.ma".
    3 include "Status.ma".
    43
    54ndefinition test: List instruction ≝
     
    164163 nnormalize; @.
    165164nqed.
     165
     166ndefinition testfinal ≝ execute five teststatus.
     167
     168nlemma hoo: testfinal = testfinal.
     169 nwhd in ⊢ (???%);
     170 nnormalize; @.
     171nqed.
Note: See TracChangeset for help on using the changeset viewer.