Changeset 156 for C-semantics/Mem.ma


Ignore:
Timestamp:
Oct 6, 2010, 4:17:57 PM (9 years ago)
Author:
campbell
Message:

pdata support

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Mem.ma

    r153 r156  
    559559
    560560ninductive pointer_compat : memory_space → memory_space → Prop ≝
    561 |  data_compat : pointer_compat  Data  Data
    562 | idata_compat : pointer_compat IData IData
    563 | xdata_compat : pointer_compat XData XData
    564 |  code_compat : pointer_compat  Code  Code
     561|  same_compat : ∀s. pointer_compat s s
     562| pxdata_compat : pointer_compat PData XData
    565563| unspecified_compat : ∀p. pointer_compat Any p
    566564| universal_compat : ∀b. pointer_compat b Any.
Note: See TracChangeset for help on using the changeset viewer.