Changeset 2108 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Jun 25, 2012, 2:39:06 PM (7 years ago)
Author:
mulligan
Message:

Various axioms closed and others moved around. Uncommented main lemma and found that it no longer compiles due to changing how we expand jumps. Problem in proof highlighted with XXX for Claudio.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r2062 r2108  
    33include "ASM/Fetch.ma".
    44include "ASM/AbstractStatus.ma".
    5 
    6 definition sign_extension: Byte → Word ≝
    7   λc.
    8     let b ≝ get_index_v ? 8 c 1 ? in
    9       [[ b; b; b; b; b; b; b; b ]] @@ c.
    10   normalize
    11   repeat (@le_S_S)
    12   @le_O_n
    13 qed.
    145   
    156lemma execute_1_technical:
Note: See TracChangeset for help on using the changeset viewer.