Ignore:
Timestamp:
Dec 1, 2010, 6:03:45 PM (9 years ago)
Author:
mulligan
Message:

Do not use ndestruct for injectivity since it introduces StreickerK that
blocks reductions.

File:
1 edited

Legend:

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

    r350 r352  
    151151 @.
    152152nqed.
    153 
    154 ndefinition testmem ≝ assembly test.
    155 
    156 nlemma foo: testmem = testmem.
    157  nnormalize; @.
    158 nqed.
    159 
    160 ndefinition teststatus ≝ load testmem initialise_status.
    161 
    162 nlemma goo: teststatus = teststatus.
    163  nnormalize; @.
    164 nqed.
    165 
    166 ndefinition testfinal ≝ execute one teststatus.
    167 
    168 nlemma hoo: (*half_add ? (program_counter teststatus)*)
    169   (bitvector_of_nat sixteen (S Z)) = (bitvector_of_nat sixteen (S Z)).
    170  (*half_add (code_memory teststatus) (program_counter teststatus). *)
    171  nwhd in ⊢ (??%?);
    172 
    173 nlemma hoo: testfinal = testfinal.
    174  nwhd in ⊢ (??%?);
    175  nnormalize; @.
    176 nqed.
Note: See TracChangeset for help on using the changeset viewer.