Changeset 2155 for src/utilities


Ignore:
Timestamp:
Jul 6, 2012, 11:25:43 AM (8 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/utilities/bindLists.ma

    r1882 r2155  
    1818
    1919definition bcons : ∀B,E.E → bind_list B E → bind_list B E ≝
    20   λB,E,e,l.[e] @@ l.
    21 
     20  λB,E,e.m_map … (cons … e).
    2221interpretation "cons blist" 'vcons l1 l2 = (bcons ?? l1 l2).
    2322
     
    4342  (bcompile U R (list E) fresh (e ::: bl2)) ≅
    4443    ! l ← bcompile … fresh bl2 ; return (e :: l).
    45       #U#R#E#fresh#e#bl2 #u
    46       >bcompile_append normalize //
     44      #U#R#E#fresh#e#bl2 #u @bcompile_bbind
    4745qed.
Note: See TracChangeset for help on using the changeset viewer.