 Timestamp:
 Mar 29, 2013, 12:53:35 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Arithmetic.ma
r2796 r3033 958 958 ∀size, m: nat. 959 959 ∀size_proof: 0 < size. 960 m < 2^size → get_index_v bool (S size) (bitvector_of_nat (S size) m) 1? = false.961 normalize in size_proof; normalize @le_S_S assumption 960 m < 2^size → get_index_v bool (S size) (bitvector_of_nat (S size) m) 0 ? = false. 961 @(transitive_le … size_proof) @le_S % 962 962 qed. 963 963 … … 1012 1012 definition sign_extension: Byte → Word ≝ 1013 1013 λc. 1014 let b ≝ get_index_v ? 8 c 1? in1014 let b ≝ get_index_v ? 8 c 0 ? in 1015 1015 [[ b; b; b; b; b; b; b; b ]] @@ c. 1016 1016 normalize
Note: See TracChangeset
for help on using the changeset viewer.