(* operatore Least Significant Bit *)
ndefinition getLSB_w24 ≝ λw:word24.getLSB_b8 (w24l w).
ndefinition setLSB_w24 ≝ λw:word24.mk_word24 (w24x w) (w24h w) (setLSB_b8 (w24l w)).
(* operatore Least Significant Bit *)
ndefinition getLSB_w24 ≝ λw:word24.getLSB_b8 (w24l w).
ndefinition setLSB_w24 ≝ λw:word24.mk_word24 (w24x w) (w24h w) (setLSB_b8 (w24l w)).