law set_view

lawful-bytes@0.1.1.0 · LAWS.bend:154

import Base
import lawful-bytes@0.1.1.0/defs.bend as D
import lawful-bytes@0.1.1.0/bytes.bend as B

154law set_view:
155  for b: D.Bytes
156  for d: Nat
157  for i: U32
158  for v: U32
159  for h: {D.ok(b, d) == True{} : Bool}
160  for hi: {Nat.is_lt(U32.to_nat(i), D.size(b)) == True{} : Bool}
161  for hv: {U32.is_lt(v, 256) == True{} : Bool}
162  {D.view(B.set(b, i, v)) == List.set(&2, U32, D.view(b), U32.to_nat(i), v) : List<&2, U32>}