law wbp1

lawful-bytes@0.1.1.0 · proof_core.bend:315

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

315law wbp1:
316  for +w: U32
317  for +v: U32
318  for +hv: {U32.is_lt(v, 256) == True{} : Bool}
319  {L4(W.put_byte(w, 1n, v)) == List.set(&2, U32, L4(w), 1n, v) : List<&2, U32>}