Changeset 3033
 Timestamp:
 Mar 29, 2013, 12:53:35 PM (7 years ago)
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

extracted/arithmetic.ml
r2775 r3033 297 297 (** val fbs_diff_rect_Type4 : 298 298 (Nat.nat > Nat.nat > 'a1) > Nat.nat > fbs_diff > 'a1 **) 299 let rec fbs_diff_rect_Type4 h_fbs_diff' x_ 1368= function299 let rec fbs_diff_rect_Type4 h_fbs_diff' x_4 = function 300 300  Fbs_diff' (n, m) > h_fbs_diff' n m 301 301 302 302 (** val fbs_diff_rect_Type5 : 303 303 (Nat.nat > Nat.nat > 'a1) > Nat.nat > fbs_diff > 'a1 **) 304 let rec fbs_diff_rect_Type5 h_fbs_diff' x_ 1371= function304 let rec fbs_diff_rect_Type5 h_fbs_diff' x_7 = function 305 305  Fbs_diff' (n, m) > h_fbs_diff' n m 306 306 307 307 (** val fbs_diff_rect_Type3 : 308 308 (Nat.nat > Nat.nat > 'a1) > Nat.nat > fbs_diff > 'a1 **) 309 let rec fbs_diff_rect_Type3 h_fbs_diff' x_1 374= function309 let rec fbs_diff_rect_Type3 h_fbs_diff' x_10 = function 310 310  Fbs_diff' (n, m) > h_fbs_diff' n m 311 311 312 312 (** val fbs_diff_rect_Type2 : 313 313 (Nat.nat > Nat.nat > 'a1) > Nat.nat > fbs_diff > 'a1 **) 314 let rec fbs_diff_rect_Type2 h_fbs_diff' x_13 77= function314 let rec fbs_diff_rect_Type2 h_fbs_diff' x_13 = function 315 315  Fbs_diff' (n, m) > h_fbs_diff' n m 316 316 317 317 (** val fbs_diff_rect_Type1 : 318 318 (Nat.nat > Nat.nat > 'a1) > Nat.nat > fbs_diff > 'a1 **) 319 let rec fbs_diff_rect_Type1 h_fbs_diff' x_1 380= function319 let rec fbs_diff_rect_Type1 h_fbs_diff' x_16 = function 320 320  Fbs_diff' (n, m) > h_fbs_diff' n m 321 321 322 322 (** val fbs_diff_rect_Type0 : 323 323 (Nat.nat > Nat.nat > 'a1) > Nat.nat > fbs_diff > 'a1 **) 324 let rec fbs_diff_rect_Type0 h_fbs_diff' x_1 383= function324 let rec fbs_diff_rect_Type0 h_fbs_diff' x_19 = function 325 325  Fbs_diff' (n, m) > h_fbs_diff' n m 326 326 … … 760 760 let b = 761 761 Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 762 (Nat.S Nat.O)))))))) c (Nat.S Nat.O)762 (Nat.S Nat.O)))))))) c Nat.O 763 763 in 764 764 Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 
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.