def bits.word_bytes

bend-osdev-mode-core@0.1.0.0 · PROOF.bend:28

import Base
import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M

28def bits.word_bytes(w: U32) -> {M.cm.word(M.cm.b0(w), M.cm.b1(w), M.cm.b2(w), M.cm.b3(w)) == w : U32}:
29  match w:
30    case U32{WCon{w0, WCon{w1, WCon{w2, WCon{w3, WCon{w4, WCon{w5, WCon{w6, WCon{w7, WCon{w8, WCon{w9, WCon{w10, WCon{w11, WCon{w12, WCon{w13, WCon{w14, WCon{w15, WCon{w16, WCon{w17, WCon{w18, WCon{w19, WCon{w20, WCon{w21, WCon{w22, WCon{w23, WCon{w24, WCon{w25, WCon{w26, WCon{w27, WCon{w28, WCon{w29, WCon{w30, WCon{w31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
31      {==}