Changeset 2155 for src/common


Ignore:
Timestamp:
Jul 6, 2012, 11:25:43 AM (7 years ago)
Author:
tranquil
Message:

updates to blocks and RTLabs to RTL translation (which sidesteps pointer arithmetics issues for now)

Joint semantics and traces momentarily broken, concentrating on syntax now

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r2111 r2155  
    834834qed. 
    835835
    836 
    837 
     836lemma map_mem_prop :
     837  ∀tag,A.∀m : identifier_map tag A.∀i.
     838  lookup ?? m i ≠ None ? → i ∈ m.
     839#p #globals #m #i
     840lapply (in_map_domain … m i)
     841cases (i∈m)
     842[ * #x #_ #_ %
     843| #EQ >EQ * #ABS @ABS %
     844] qed.
     845
     846
     847
Note: See TracChangeset for help on using the changeset viewer.