law block_of_bytes_of

bend-osdev-mode-core@0.1.0.0 · LAWS.bend:128

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

128# the block of a block's bytes is the block
129law block_of_bytes_of:
130  for b: M.CmBlock
131  {M.cm.block_of(M.cm.bytes_of(b)) == b : M.CmBlock}

Uses (4)

Used by (0)

No other definition uses this definition.