Changeset 2032 for src/RTLabs/RTLabsToRTL.ma
 Timestamp:
 Jun 8, 2012, 4:32:03 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLabsToRTL.ma
r1995 r2032 134 134 [ I8 ⇒ λint. ?  I16 ⇒ λint. ?  I32 ⇒ λint. ? ]. 135 135 [ %[@[int]] // 136  %[@(let 〈h,l〉 ≝ split ? 8 … int in [l;h])] cases (split ????) //137  %[@(let 〈h1,l〉 ≝ split ? 8 … int in138 let 〈h2,l〉 ≝ split ? 8 … l in139 let 〈h3,l〉 ≝ split ? 8 … l in136  %[@(let 〈h,l〉 ≝ vsplit ? 8 … int in [l;h])] cases (vsplit ????) // 137  %[@(let 〈h1,l〉 ≝ vsplit ? 8 … int in 138 let 〈h2,l〉 ≝ vsplit ? 8 … l in 139 let 〈h3,l〉 ≝ vsplit ? 8 … l in 140 140 [l;h3;h2;h1])] 141 cases ( split ????) #h1 #l normalize142 cases ( split ????) #h2 #l normalize143 cases ( split ????) // ]141 cases (vsplit ????) #h1 #l normalize 142 cases (vsplit ????) #h2 #l normalize 143 cases (vsplit ????) // ] 144 144 qed. 145 145 … … 533 533 λtranslates: list ?. 534 534 λsrcr2i: register. 535 let 〈tmp_destrs1, tmp_destrs2〉 ≝ split … tmp_destrs i i_prf in535 let 〈tmp_destrs1, tmp_destrs2〉 ≝ vsplit … tmp_destrs i i_prf in 536 536 let tmp_destrs2' ≝ 537 537 match tmp_destrs2 with
Note: See TracChangeset
for help on using the changeset viewer.