Ignore:
Timestamp:
Nov 28, 2012, 5:57:38 PM (7 years ago)
Author:
garnier
Message:

Continuing work on simulation in Clight/Cminor?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/memoryInjections.ma

    r2483 r2500  
    265265  λo1,o2. mk_offset (addition_n ? (offv o1) (offv o2)).
    266266
    267 lemma offset_plus_0 : ∀o. offset_plus o (mk_offset (zero ?)) = o.
     267lemma offset_plus_0 : ∀o. offset_plus (mk_offset (zero ?)) o = o.
    268268* #o
    269269whd in match (offset_plus ??);
     270>commutative_addition_n
    270271>addition_n_0 @refl
    271272qed.
Note: See TracChangeset for help on using the changeset viewer.