-(* operatore Most Significant Bit *)
-ndefinition getMSB_ex ≝
-λe:exadecim.match e with
- [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
- | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
- | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
- | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ].
-
-ndefinition setMSB_ex ≝
-λe:exadecim.match e with
- [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB
- | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
- | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
- | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ].
-
-ndefinition clrMSB_ex ≝
-λe:exadecim.match e with
- [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
- | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
- | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
- | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ].
-
-(* operatore Least Significant Bit *)
-ndefinition getLSB_ex ≝
-λe:exadecim.match e with
- [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ false | x3 ⇒ true
- | x4 ⇒ false | x5 ⇒ true | x6 ⇒ false | x7 ⇒ true
- | x8 ⇒ false | x9 ⇒ true | xA ⇒ false | xB ⇒ true
- | xC ⇒ false | xD ⇒ true | xE ⇒ false | xF ⇒ true ].
-
-ndefinition setLSB_ex ≝
-λe:exadecim.match e with
- [ x0 ⇒ x1 | x1 ⇒ x1 | x2 ⇒ x3 | x3 ⇒ x3
- | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
- | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB
- | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ].
-
-ndefinition clrLSB_ex ≝
-λe:exadecim.match e with
- [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
- | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
- | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA
- | xC ⇒ xC | xD ⇒ xC | xE ⇒ xE | xF ⇒ xE ].
-