law rep_pack

lawful-bytes@0.1.1.0 · proof_fast_w2.bend:214

import Base
import lawful-words@0.1.0.0/defs.bend as W
import lawful-bytes@0.1.1.0/fast.bend as FA

214law rep_pack:
215  for +c: U32
216  for +hc: {U32.is_lt(c, 256) == True{} : Bool}
217  {FA.rep(c) == W.pack4(c, c, c, c) : U32}