-λw:word24.match shl_b8 (w24l w) with
- [ pair wl' c' ⇒ match rcl_b8 (w24h w) c' with
- [ pair wh' c'' ⇒ match rcl_b8 (w24x w) c'' with
- [ pair wx' c''' ⇒ match c''' with
- [ true ⇒ mk_word24 wx' wh' (or_b8 (mk_byte8 x0 x1) wl')
- | false ⇒ mk_word24 wx' wh' wl' ]]]].
-
-(* operatore rotazione sinistra n-volte *)
-nlet rec rol_w24_n (w:word24) (t:bitrigesim) (rt:rec_bitrigesim t) on rt ≝
- match rt with
- [ bi_O ⇒ w
- | bi_S t' n' ⇒ rol_w24_n (rol_w24 w) t' n' ].