Ignore:
Timestamp:
Feb 11, 2011, 4:45:37 PM (9 years ago)
Author:
campbell
Message:

pointer_compat is a little more natural if it takes that block rather than
the block's region.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/CexecComplete.ma

    r498 r499  
    3939] qed.
    4040
    41 lemma is_pointer_compat_true: ∀m,b,sp.
    42   pointer_compat (block_region m b) sp →
    43   is_pointer_compat (block_region m b) sp = true.
    44 #m #b #sp #H whd in ⊢ (??%?);
    45 elim (pointer_compat_dec (block_region m b) sp);
     41lemma is_pointer_compat_true: ∀b,sp.
     42  pointer_compat b sp →
     43  is_pointer_compat b sp = true.
     44#b #sp #H whd in ⊢ (??%?);
     45elim (pointer_compat_dec b sp);
    4646[ //
    4747| #H' @False_ind @(absurd … H H')
Note: See TracChangeset for help on using the changeset viewer.