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.