Changeset 497


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

Remove bogus pointer compatibility case.

File:
1 edited

Legend:

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

    r496 r497  
    591591|        same_compat : ∀s. pointer_compat s s
    592592|      pxdata_compat : pointer_compat PData XData
    593 | unspecified_compat : ∀p. pointer_compat Any p
    594593|   universal_compat : ∀b. pointer_compat b Any.
    595594
    596595lemma pointer_compat_dec : ∀b,p. pointer_compat b p + ¬pointer_compat b p.
    597 #b #p cases b;
    598 [ 1: %1 //;
    599 | *: cases p; /2/; %2 % #H inversion H; #e1 #e2 destruct; #e3 destruct;
    600 ] qed.
     596#b #p cases b
     597cases p /2/ %2 % #H inversion H #e1 #e2 destruct #e3 destruct
     598qed.
    601599
    602600definition is_pointer_compat : region → region → bool ≝
Note: See TracChangeset for help on using the changeset viewer.