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

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLabsToRTL_paolo.ma
r1882 r2032 119 119 [ I8 ⇒ λint. ?  I16 ⇒ λint. ?  I32 ⇒ λint. ? ]. 120 120 [ %[@[int]] // 121  %[@(let 〈h,l〉 ≝ split ? 8 … int in [l;h])] cases (split ????) normalize //122  %[@(let 〈h1,l〉 ≝ split ? 8 … int in123 let 〈h2,l〉 ≝ split ? 8 … l in124 let 〈h3,l〉 ≝ split ? 8 … l in121  %[@(let 〈h,l〉 ≝ vsplit ? 8 … int in [l;h])] cases (vsplit ????) normalize // 122  %[@(let 〈h1,l〉 ≝ vsplit ? 8 … int in 123 let 〈h2,l〉 ≝ vsplit ? 8 … l in 124 let 〈h3,l〉 ≝ vsplit ? 8 … l in 125 125 [l;h3;h2;h1])] 126 cases ( split ????) #h1 #l normalize127 cases ( split ????) #h2 #l normalize128 cases ( split ????) // ]126 cases (vsplit ????) #h1 #l normalize 127 cases (vsplit ????) #h2 #l normalize 128 cases (vsplit ????) // ] 129 129 qed. 130 130
Note: See TracChangeset
for help on using the changeset viewer.