def byte

lawful-words@0.1.0.0 · defs.bend:20

import Base

20# Byte j of a word (byte 0 is the lowest): (w >> 8j) & 255.
21def byte(w: U32, j: Nat) -> U32:
22  U32.and(U32.shrn(w, Nat.mul(8n, j)), 255)