Changeset 1646 for src/ASM/Arithmetic.ma
 Timestamp:
 Jan 16, 2012, 3:04:14 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Arithmetic.ma
r1599 r1646 1 1 include "ASM/BitVector.ma". 2 2 include "ASM/Util.ma". 3 4 definition addr16_of_addr11: Word → Word11 → Word ≝ 5 λpc: Word. 6 λa: Word11. 7 let 〈pc_upper, ignore〉 ≝ split … 8 8 pc in 8 let 〈n1, n2〉 ≝ split … 4 4 pc_upper in 9 let 〈b123, b〉 ≝ split … 3 8 a in 10 let b1 ≝ get_index_v … b123 0 ? in 11 let b2 ≝ get_index_v … b123 1 ? in 12 let b3 ≝ get_index_v … b123 2 ? in 13 let p5 ≝ get_index_v … n2 0 ? in 14 (n1 @@ [[ p5; b1; b2; b3 ]]) @@ b. 15 // 16 qed. 3 17 4 18 definition nat_of_bool ≝
Note: See TracChangeset
for help on using the changeset viewer.