2 inductive exadecim : Type ≝
20 inductive bool : Type ≝ true :bool | false : bool .
26 [ x0 ⇒ match e2 with [ x0 ⇒ true | _ ⇒ false ]
27 | x1 ⇒ match e2 with [ x1 ⇒ true | _ ⇒ false ]
28 | x2 ⇒ match e2 with [ x2 ⇒ true | _ ⇒ false ]
29 | x3 ⇒ match e2 with [ x3 ⇒ true | _ ⇒ false ]
30 | x4 ⇒ match e2 with [ x4 ⇒ true | _ ⇒ false ]
31 | x5 ⇒ match e2 with [ x5 ⇒ true | _ ⇒ false ]
32 | x6 ⇒ match e2 with [ x6 ⇒ true | _ ⇒ false ]
33 | x7 ⇒ match e2 with [ x7 ⇒ true | _ ⇒ false ]
34 | x8 ⇒ match e2 with [ x8 ⇒ true | _ ⇒ false ]
35 | x9 ⇒ match e2 with [ x9 ⇒ true | _ ⇒ false ]
36 | xA ⇒ match e2 with [ xA ⇒ true | _ ⇒ false ]
37 | xB ⇒ match e2 with [ xB ⇒ true | _ ⇒ false ]
38 | xC ⇒ match e2 with [ xC ⇒ true | _ ⇒ false ]
39 | xD ⇒ match e2 with [ xD ⇒ true | _ ⇒ false ]
40 | xE ⇒ match e2 with [ xE ⇒ true | _ ⇒ false ]
41 | xF ⇒ match e2 with [ xF ⇒ true | _ ⇒ false ]
47 [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
48 | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ].
57 notation "〈x,y〉" non associative with precedence 80
58 for @{ 'mk_byte8 $x $y }.
59 interpretation "mk_byte8" 'mk_byte8 x y = (mk_byte8 x y).
61 definition andb ≝ λa,b.match a with [ true ⇒ b | _ ⇒ false ].
63 definition eq_b8 ≝ λb1,b2:byte8.andb (eq_ex (b8h b1) (b8h b2)) (eq_ex (b8l b1) (b8l b2)).
65 λb:byte8.match eq_ex (b8l b) xF with
66 [ true ⇒ mk_byte8 (succ_ex (b8h b)) (succ_ex (b8l b))
67 | false ⇒ mk_byte8 (b8h b) (succ_ex (b8l b)) ].
69 record word16 : Type ≝
76 notation "〈x:y〉" non associative with precedence 80
77 for @{ 'mk_word16 $x $y }.
78 interpretation "mk_word16" 'mk_word16 x y = (mk_word16 x y).
84 match eq_b8 (w16l w) (mk_byte8 xF xF) with
85 [ true ⇒ mk_word16 (succ_b8 (w16h w)) (succ_b8 (w16l w))
86 | false ⇒ mk_word16 (w16h w) (succ_b8 (w16l w)) ].
88 inductive eq (A:Type) (a:A) : A → Prop ≝ refl_eq : eq A a a.
90 interpretation "aa" 'eq t a b = (eq t a b).