law lo_from_u32

bend-osdev-word64@0.1.1.0 · LAWS.bend:39

import Base
import bend-osdev-word64@0.1.1.0/word64.bend as W

39# For every 32-bit a: from_u32 then lo gives a back.
40law lo_from_u32:
41  for a: U32
42  {W.W64.lo(W.W64.from_u32(a)) == a : U32}