; a16_9 : T ; a16_10 : T ; a16_11 : T ; a16_12 : T
; a16_13 : T ; a16_14 : T ; a16_15 : T ; a16_16 : T }.
+(* operatore uguaglianza *)
+ndefinition eq_ar16 ≝
+λT.λf:T → T → bool.λa1,a2:Array16T T.
+ (f (a16_1 ? a1) (a16_1 ? a2)) ⊗ (f (a16_2 ? a1) (a16_2 ? a2)) ⊗
+ (f (a16_3 ? a1) (a16_3 ? a2)) ⊗ (f (a16_4 ? a1) (a16_4 ? a2)) ⊗
+ (f (a16_5 ? a1) (a16_5 ? a2)) ⊗ (f (a16_6 ? a1) (a16_6 ? a2)) ⊗
+ (f (a16_7 ? a1) (a16_7 ? a2)) ⊗ (f (a16_8 ? a1) (a16_8 ? a2)) ⊗
+ (f (a16_9 ? a1) (a16_9 ? a2)) ⊗ (f (a16_10 ? a1) (a16_10 ? a2)) ⊗
+ (f (a16_11 ? a1) (a16_11 ? a2)) ⊗ (f (a16_12 ? a1) (a16_12 ? a2)) ⊗
+ (f (a16_13 ? a1) (a16_13 ? a2)) ⊗ (f (a16_14 ? a1) (a16_14 ? a2)) ⊗
+ (f (a16_15 ? a1) (a16_15 ? a2)) ⊗ (f (a16_16 ? a1) (a16_16 ? a2)).
+
(* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
(* posso definire un getter a matrice sull'array *)
{ a8_1 : T ; a8_2 : T ; a8_3 : T ; a8_4 : T
; a8_5 : T ; a8_6 : T ; a8_7 : T ; a8_8 : T }.
+(* operatore uguaglianza *)
+ndefinition eq_ar8 ≝
+λT.λf:T → T → bool.λa1,a2:Array8T T.
+ (f (a8_1 ? a1) (a8_1 ? a2)) ⊗ (f (a8_2 ? a1) (a8_2 ? a2)) ⊗
+ (f (a8_3 ? a1) (a8_3 ? a2)) ⊗ (f (a8_4 ? a1) (a8_4 ? a2)) ⊗
+ (f (a8_5 ? a1) (a8_5 ? a2)) ⊗ (f (a8_6 ? a1) (a8_6 ? a2)) ⊗
+ (f (a8_7 ? a1) (a8_7 ? a2)) ⊗ (f (a8_8 ? a1) (a8_8 ? a2)).
+
(* abbiamo gia' gli ottali come tipo induttivo quindi: *)
(* posso definire un getter a matrice sull'array *)
ndefinition getn_array8T ≝
let e06 ≝ (a8_7 T p) in
let e07 ≝ (a8_8 T p) in
match n with
- [ o0 ⇒ mk_Array8T T e07 e06 e05 e04 e03 e02 e01 v
- | o1 ⇒ mk_Array8T T e07 e06 e05 e04 e03 e02 v e00
- | o2 ⇒ mk_Array8T T e07 e06 e05 e04 e03 v e01 e00
- | o3 ⇒ mk_Array8T T e07 e06 e05 e04 v e02 e01 e00
- | o4 ⇒ mk_Array8T T e07 e06 e05 v e03 e02 e01 e00
- | o5 ⇒ mk_Array8T T e07 e06 v e04 e03 e02 e01 e00
- | o6 ⇒ mk_Array8T T e07 v e05 e04 e03 e02 e01 e00
- | o7 ⇒ mk_Array8T T v e06 e05 e04 e03 e02 e01 e00
+ [ o0 ⇒ mk_Array8T T v e01 e02 e03 e04 e05 e06 e07
+ | o1 ⇒ mk_Array8T T e00 v e02 e03 e04 e05 e06 e07
+ | o2 ⇒ mk_Array8T T e00 e01 v e03 e04 e05 e06 e07
+ | o3 ⇒ mk_Array8T T e00 e01 e02 v e04 e05 e06 e07
+ | o4 ⇒ mk_Array8T T e00 e01 e02 e03 v e05 e06 e07
+ | o5 ⇒ mk_Array8T T e00 e01 e02 e03 e04 v e06 e07
+ | o6 ⇒ mk_Array8T T e00 e01 e02 e03 e04 e05 v e07
+ | o7 ⇒ mk_Array8T T e00 e01 e02 e03 e04 e05 e06 v
].
(* lettura byte *)
ndefinition byte8_of_bits ≝
λp:Array8T bool.
mk_byte8
- (or_ex (match a8_8 ? p with [ true ⇒ x8 | false ⇒ x0 ])
- (or_ex (match a8_7 ? p with [ true ⇒ x4 | false ⇒ x0 ])
- (or_ex (match a8_6 ? p with [ true ⇒ x2 | false ⇒ x0 ])
- (match a8_5 ? p with [ true ⇒ x1 | false ⇒ x0 ]))))
- (or_ex (match a8_4 ? p with [ true ⇒ x8 | false ⇒ x0 ])
- (or_ex (match a8_3 ? p with [ true ⇒ x4 | false ⇒ x0 ])
- (or_ex (match a8_2 ? p with [ true ⇒ x2 | false ⇒ x0 ])
- (match a8_1 ? p with [ true ⇒ x1 | false ⇒ x0 ])))).
+ (or_ex (match a8_1 ? p with [ true ⇒ x8 | false ⇒ x0 ])
+ (or_ex (match a8_2 ? p with [ true ⇒ x4 | false ⇒ x0 ])
+ (or_ex (match a8_3 ? p with [ true ⇒ x2 | false ⇒ x0 ])
+ (match a8_4 ? p with [ true ⇒ x1 | false ⇒ x0 ]))))
+ (or_ex (match a8_5 ? p with [ true ⇒ x8 | false ⇒ x0 ])
+ (or_ex (match a8_6 ? p with [ true ⇒ x4 | false ⇒ x0 ])
+ (or_ex (match a8_7 ? p with [ true ⇒ x2 | false ⇒ x0 ])
+ (match a8_8 ? p with [ true ⇒ x1 | false ⇒ x0 ])))).
(* scrittura byte *)
+ndefinition bits_of_exadecim ≝
+λe:exadecim.match e with
+ [ x0 ⇒ quadruple … false false false false
+ | x1 ⇒ quadruple … false false false true
+ | x2 ⇒ quadruple … false false true false
+ | x3 ⇒ quadruple … false false true true
+ | x4 ⇒ quadruple … false true false false
+ | x5 ⇒ quadruple … false true false true
+ | x6 ⇒ quadruple … false true true false
+ | x7 ⇒ quadruple … false true true true
+ | x8 ⇒ quadruple … true false false false
+ | x9 ⇒ quadruple … true false false true
+ | xA ⇒ quadruple … true false true false
+ | xB ⇒ quadruple … true false true true
+ | xC ⇒ quadruple … true true false false
+ | xD ⇒ quadruple … true true false true
+ | xE ⇒ quadruple … true true true false
+ | xF ⇒ quadruple … true true true true
+ ].
ndefinition bits_of_byte8 ≝
-λp:byte8.
- match b8h p with
- [ x0 ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool false false false false false false false false
- | x1 ⇒ mk_Array8T bool false false false false false false false true
- | x2 ⇒ mk_Array8T bool false false false false false false true false
- | x3 ⇒ mk_Array8T bool false false false false false false true true
- | x4 ⇒ mk_Array8T bool false false false false false true false false
- | x5 ⇒ mk_Array8T bool false false false false false true false true
- | x6 ⇒ mk_Array8T bool false false false false false true true false
- | x7 ⇒ mk_Array8T bool false false false false false true true true
- | x8 ⇒ mk_Array8T bool false false false false true false false false
- | x9 ⇒ mk_Array8T bool false false false false true false false true
- | xA ⇒ mk_Array8T bool false false false false true false true false
- | xB ⇒ mk_Array8T bool false false false false true false true true
- | xC ⇒ mk_Array8T bool false false false false true true false false
- | xD ⇒ mk_Array8T bool false false false false true true false true
- | xE ⇒ mk_Array8T bool false false false false true true true false
- | xF ⇒ mk_Array8T bool false false false false true true true true ]
- | x1 ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool false false false true false false false false
- | x1 ⇒ mk_Array8T bool false false false true false false false true
- | x2 ⇒ mk_Array8T bool false false false true false false true false
- | x3 ⇒ mk_Array8T bool false false false true false false true true
- | x4 ⇒ mk_Array8T bool false false false true false true false false
- | x5 ⇒ mk_Array8T bool false false false true false true false true
- | x6 ⇒ mk_Array8T bool false false false true false true true false
- | x7 ⇒ mk_Array8T bool false false false true false true true true
- | x8 ⇒ mk_Array8T bool false false false true true false false false
- | x9 ⇒ mk_Array8T bool false false false true true false false true
- | xA ⇒ mk_Array8T bool false false false true true false true false
- | xB ⇒ mk_Array8T bool false false false true true false true true
- | xC ⇒ mk_Array8T bool false false false true true true false false
- | xD ⇒ mk_Array8T bool false false false true true true false true
- | xE ⇒ mk_Array8T bool false false false true true true true false
- | xF ⇒ mk_Array8T bool false false false true true true true true ]
- | x2 ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool false false true false false false false false
- | x1 ⇒ mk_Array8T bool false false true false false false false true
- | x2 ⇒ mk_Array8T bool false false true false false false true false
- | x3 ⇒ mk_Array8T bool false false true false false false true true
- | x4 ⇒ mk_Array8T bool false false true false false true false false
- | x5 ⇒ mk_Array8T bool false false true false false true false true
- | x6 ⇒ mk_Array8T bool false false true false false true true false
- | x7 ⇒ mk_Array8T bool false false true false false true true true
- | x8 ⇒ mk_Array8T bool false false true false true false false false
- | x9 ⇒ mk_Array8T bool false false true false true false false true
- | xA ⇒ mk_Array8T bool false false true false true false true false
- | xB ⇒ mk_Array8T bool false false true false true false true true
- | xC ⇒ mk_Array8T bool false false true false true true false false
- | xD ⇒ mk_Array8T bool false false true false true true false true
- | xE ⇒ mk_Array8T bool false false true false true true true false
- | xF ⇒ mk_Array8T bool false false true false true true true true ]
- | x3 ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool false false true true false false false false
- | x1 ⇒ mk_Array8T bool false false true true false false false true
- | x2 ⇒ mk_Array8T bool false false true true false false true false
- | x3 ⇒ mk_Array8T bool false false true true false false true true
- | x4 ⇒ mk_Array8T bool false false true true false true false false
- | x5 ⇒ mk_Array8T bool false false true true false true false true
- | x6 ⇒ mk_Array8T bool false false true true false true true false
- | x7 ⇒ mk_Array8T bool false false true true false true true true
- | x8 ⇒ mk_Array8T bool false false true true true false false false
- | x9 ⇒ mk_Array8T bool false false true true true false false true
- | xA ⇒ mk_Array8T bool false false true true true false true false
- | xB ⇒ mk_Array8T bool false false true true true false true true
- | xC ⇒ mk_Array8T bool false false true true true true false false
- | xD ⇒ mk_Array8T bool false false true true true true false true
- | xE ⇒ mk_Array8T bool false false true true true true true false
- | xF ⇒ mk_Array8T bool false false true true true true true true ]
- | x4 ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool false true false false false false false false
- | x1 ⇒ mk_Array8T bool false true false false false false false true
- | x2 ⇒ mk_Array8T bool false true false false false false true false
- | x3 ⇒ mk_Array8T bool false true false false false false true true
- | x4 ⇒ mk_Array8T bool false true false false false true false false
- | x5 ⇒ mk_Array8T bool false true false false false true false true
- | x6 ⇒ mk_Array8T bool false true false false false true true false
- | x7 ⇒ mk_Array8T bool false true false false false true true true
- | x8 ⇒ mk_Array8T bool false true false false true false false false
- | x9 ⇒ mk_Array8T bool false true false false true false false true
- | xA ⇒ mk_Array8T bool false true false false true false true false
- | xB ⇒ mk_Array8T bool false true false false true false true true
- | xC ⇒ mk_Array8T bool false true false false true true false false
- | xD ⇒ mk_Array8T bool false true false false true true false true
- | xE ⇒ mk_Array8T bool false true false false true true true false
- | xF ⇒ mk_Array8T bool false true false false true true true true ]
- | x5 ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool false true false true false false false false
- | x1 ⇒ mk_Array8T bool false true false true false false false true
- | x2 ⇒ mk_Array8T bool false true false true false false true false
- | x3 ⇒ mk_Array8T bool false true false true false false true true
- | x4 ⇒ mk_Array8T bool false true false true false true false false
- | x5 ⇒ mk_Array8T bool false true false true false true false true
- | x6 ⇒ mk_Array8T bool false true false true false true true false
- | x7 ⇒ mk_Array8T bool false true false true false true true true
- | x8 ⇒ mk_Array8T bool false true false true true false false false
- | x9 ⇒ mk_Array8T bool false true false true true false false true
- | xA ⇒ mk_Array8T bool false true false true true false true false
- | xB ⇒ mk_Array8T bool false true false true true false true true
- | xC ⇒ mk_Array8T bool false true false true true true false false
- | xD ⇒ mk_Array8T bool false true false true true true false true
- | xE ⇒ mk_Array8T bool false true false true true true true false
- | xF ⇒ mk_Array8T bool false true false true true true true true ]
- | x6 ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool false true true false false false false false
- | x1 ⇒ mk_Array8T bool false true true false false false false true
- | x2 ⇒ mk_Array8T bool false true true false false false true false
- | x3 ⇒ mk_Array8T bool false true true false false false true true
- | x4 ⇒ mk_Array8T bool false true true false false true false false
- | x5 ⇒ mk_Array8T bool false true true false false true false true
- | x6 ⇒ mk_Array8T bool false true true false false true true false
- | x7 ⇒ mk_Array8T bool false true true false false true true true
- | x8 ⇒ mk_Array8T bool false true true false true false false false
- | x9 ⇒ mk_Array8T bool false true true false true false false true
- | xA ⇒ mk_Array8T bool false true true false true false true false
- | xB ⇒ mk_Array8T bool false true true false true false true true
- | xC ⇒ mk_Array8T bool false true true false true true false false
- | xD ⇒ mk_Array8T bool false true true false true true false true
- | xE ⇒ mk_Array8T bool false true true false true true true false
- | xF ⇒ mk_Array8T bool false true true false true true true true ]
- | x7 ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool false true true true false false false false
- | x1 ⇒ mk_Array8T bool false true true true false false false true
- | x2 ⇒ mk_Array8T bool false true true true false false true false
- | x3 ⇒ mk_Array8T bool false true true true false false true true
- | x4 ⇒ mk_Array8T bool false true true true false true false false
- | x5 ⇒ mk_Array8T bool false true true true false true false true
- | x6 ⇒ mk_Array8T bool false true true true false true true false
- | x7 ⇒ mk_Array8T bool false true true true false true true true
- | x8 ⇒ mk_Array8T bool false true true true true false false false
- | x9 ⇒ mk_Array8T bool false true true true true false false true
- | xA ⇒ mk_Array8T bool false true true true true false true false
- | xB ⇒ mk_Array8T bool false true true true true false true true
- | xC ⇒ mk_Array8T bool false true true true true true false false
- | xD ⇒ mk_Array8T bool false true true true true true false true
- | xE ⇒ mk_Array8T bool false true true true true true true false
- | xF ⇒ mk_Array8T bool false true true true true true true true ]
- | x8 ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool true false false false false false false false
- | x1 ⇒ mk_Array8T bool true false false false false false false true
- | x2 ⇒ mk_Array8T bool true false false false false false true false
- | x3 ⇒ mk_Array8T bool true false false false false false true true
- | x4 ⇒ mk_Array8T bool true false false false false true false false
- | x5 ⇒ mk_Array8T bool true false false false false true false true
- | x6 ⇒ mk_Array8T bool true false false false false true true false
- | x7 ⇒ mk_Array8T bool true false false false false true true true
- | x8 ⇒ mk_Array8T bool true false false false true false false false
- | x9 ⇒ mk_Array8T bool true false false false true false false true
- | xA ⇒ mk_Array8T bool true false false false true false true false
- | xB ⇒ mk_Array8T bool true false false false true false true true
- | xC ⇒ mk_Array8T bool true false false false true true false false
- | xD ⇒ mk_Array8T bool true false false false true true false true
- | xE ⇒ mk_Array8T bool true false false false true true true false
- | xF ⇒ mk_Array8T bool true false false false true true true true ]
- | x9 ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool true false false true false false false false
- | x1 ⇒ mk_Array8T bool true false false true false false false true
- | x2 ⇒ mk_Array8T bool true false false true false false true false
- | x3 ⇒ mk_Array8T bool true false false true false false true true
- | x4 ⇒ mk_Array8T bool true false false true false true false false
- | x5 ⇒ mk_Array8T bool true false false true false true false true
- | x6 ⇒ mk_Array8T bool true false false true false true true false
- | x7 ⇒ mk_Array8T bool true false false true false true true true
- | x8 ⇒ mk_Array8T bool true false false true true false false false
- | x9 ⇒ mk_Array8T bool true false false true true false false true
- | xA ⇒ mk_Array8T bool true false false true true false true false
- | xB ⇒ mk_Array8T bool true false false true true false true true
- | xC ⇒ mk_Array8T bool true false false true true true false false
- | xD ⇒ mk_Array8T bool true false false true true true false true
- | xE ⇒ mk_Array8T bool true false false true true true true false
- | xF ⇒ mk_Array8T bool true false false true true true true true ]
- | xA ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool true false true false false false false false
- | x1 ⇒ mk_Array8T bool true false true false false false false true
- | x2 ⇒ mk_Array8T bool true false true false false false true false
- | x3 ⇒ mk_Array8T bool true false true false false false true true
- | x4 ⇒ mk_Array8T bool true false true false false true false false
- | x5 ⇒ mk_Array8T bool true false true false false true false true
- | x6 ⇒ mk_Array8T bool true false true false false true true false
- | x7 ⇒ mk_Array8T bool true false true false false true true true
- | x8 ⇒ mk_Array8T bool true false true false true false false false
- | x9 ⇒ mk_Array8T bool true false true false true false false true
- | xA ⇒ mk_Array8T bool true false true false true false true false
- | xB ⇒ mk_Array8T bool true false true false true false true true
- | xC ⇒ mk_Array8T bool true false true false true true false false
- | xD ⇒ mk_Array8T bool true false true false true true false true
- | xE ⇒ mk_Array8T bool true false true false true true true false
- | xF ⇒ mk_Array8T bool true false true false true true true true ]
- | xB ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool true false true true false false false false
- | x1 ⇒ mk_Array8T bool true false true true false false false true
- | x2 ⇒ mk_Array8T bool true false true true false false true false
- | x3 ⇒ mk_Array8T bool true false true true false false true true
- | x4 ⇒ mk_Array8T bool true false true true false true false false
- | x5 ⇒ mk_Array8T bool true false true true false true false true
- | x6 ⇒ mk_Array8T bool true false true true false true true false
- | x7 ⇒ mk_Array8T bool true false true true false true true true
- | x8 ⇒ mk_Array8T bool true false true true true false false false
- | x9 ⇒ mk_Array8T bool true false true true true false false true
- | xA ⇒ mk_Array8T bool true false true true true false true false
- | xB ⇒ mk_Array8T bool true false true true true false true true
- | xC ⇒ mk_Array8T bool true false true true true true false false
- | xD ⇒ mk_Array8T bool true false true true true true false true
- | xE ⇒ mk_Array8T bool true false true true true true true false
- | xF ⇒ mk_Array8T bool true false true true true true true true ]
- | xC ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool true true false false false false false false
- | x1 ⇒ mk_Array8T bool true true false false false false false true
- | x2 ⇒ mk_Array8T bool true true false false false false true false
- | x3 ⇒ mk_Array8T bool true true false false false false true true
- | x4 ⇒ mk_Array8T bool true true false false false true false false
- | x5 ⇒ mk_Array8T bool true true false false false true false true
- | x6 ⇒ mk_Array8T bool true true false false false true true false
- | x7 ⇒ mk_Array8T bool true true false false false true true true
- | x8 ⇒ mk_Array8T bool true true false false true false false false
- | x9 ⇒ mk_Array8T bool true true false false true false false true
- | xA ⇒ mk_Array8T bool true true false false true false true false
- | xB ⇒ mk_Array8T bool true true false false true false true true
- | xC ⇒ mk_Array8T bool true true false false true true false false
- | xD ⇒ mk_Array8T bool true true false false true true false true
- | xE ⇒ mk_Array8T bool true true false false true true true false
- | xF ⇒ mk_Array8T bool true true false false true true true true ]
- | xD ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool true true false true false false false false
- | x1 ⇒ mk_Array8T bool true true false true false false false true
- | x2 ⇒ mk_Array8T bool true true false true false false true false
- | x3 ⇒ mk_Array8T bool true true false true false false true true
- | x4 ⇒ mk_Array8T bool true true false true false true false false
- | x5 ⇒ mk_Array8T bool true true false true false true false true
- | x6 ⇒ mk_Array8T bool true true false true false true true false
- | x7 ⇒ mk_Array8T bool true true false true false true true true
- | x8 ⇒ mk_Array8T bool true true false true true false false false
- | x9 ⇒ mk_Array8T bool true true false true true false false true
- | xA ⇒ mk_Array8T bool true true false true true false true false
- | xB ⇒ mk_Array8T bool true true false true true false true true
- | xC ⇒ mk_Array8T bool true true false true true true false false
- | xD ⇒ mk_Array8T bool true true false true true true false true
- | xE ⇒ mk_Array8T bool true true false true true true true false
- | xF ⇒ mk_Array8T bool true true false true true true true true ]
- | xE ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool true true true false false false false false
- | x1 ⇒ mk_Array8T bool true true true false false false false true
- | x2 ⇒ mk_Array8T bool true true true false false false true false
- | x3 ⇒ mk_Array8T bool true true true false false false true true
- | x4 ⇒ mk_Array8T bool true true true false false true false false
- | x5 ⇒ mk_Array8T bool true true true false false true false true
- | x6 ⇒ mk_Array8T bool true true true false false true true false
- | x7 ⇒ mk_Array8T bool true true true false false true true true
- | x8 ⇒ mk_Array8T bool true true true false true false false false
- | x9 ⇒ mk_Array8T bool true true true false true false false true
- | xA ⇒ mk_Array8T bool true true true false true false true false
- | xB ⇒ mk_Array8T bool true true true false true false true true
- | xC ⇒ mk_Array8T bool true true true false true true false false
- | xD ⇒ mk_Array8T bool true true true false true true false true
- | xE ⇒ mk_Array8T bool true true true false true true true false
- | xF ⇒ mk_Array8T bool true true true false true true true true ]
- | xF ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool true true true true false false false false
- | x1 ⇒ mk_Array8T bool true true true true false false false true
- | x2 ⇒ mk_Array8T bool true true true true false false true false
- | x3 ⇒ mk_Array8T bool true true true true false false true true
- | x4 ⇒ mk_Array8T bool true true true true false true false false
- | x5 ⇒ mk_Array8T bool true true true true false true false true
- | x6 ⇒ mk_Array8T bool true true true true false true true false
- | x7 ⇒ mk_Array8T bool true true true true false true true true
- | x8 ⇒ mk_Array8T bool true true true true true false false false
- | x9 ⇒ mk_Array8T bool true true true true true false false true
- | xA ⇒ mk_Array8T bool true true true true true false true false
- | xB ⇒ mk_Array8T bool true true true true true false true true
- | xC ⇒ mk_Array8T bool true true true true true true false false
- | xD ⇒ mk_Array8T bool true true true true true true false true
- | xE ⇒ mk_Array8T bool true true true true true true true false
- | xF ⇒ mk_Array8T bool true true true true true true true true ]
- ].
+λb:byte8.
+ mk_Array8T ? (fst4T … (bits_of_exadecim (b8h b)))
+ (snd4T … (bits_of_exadecim (b8h b)))
+ (thd4T … (bits_of_exadecim (b8h b)))
+ (fth4T … (bits_of_exadecim (b8h b)))
+ (fst4T … (bits_of_exadecim (b8l b)))
+ (snd4T … (bits_of_exadecim (b8l b)))
+ (thd4T … (bits_of_exadecim (b8l b)))
+ (fth4T … (bits_of_exadecim (b8l b))).
projects / helm.git / blobdiff