law wbp2

lawful-bytes@0.1.1.0 · proof_core.bend:332

import Base
import lawful-words@0.1.0.0/defs.bend as W

332law wbp2:
333  for +w: U32
334  for +v: U32
335  for +hv: {U32.is_lt(v, 256) == True{} : Bool}
336  {L4(W.put_byte(w, 2n, v)) == List.set(&2, U32, L4(w), 2n, v) : List<&2, U32>}