law set_ok

lawful-bytes@0.1.1.0 · LAWS.bend:164

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

164law set_ok:
165  for b: D.Bytes
166  for d: Nat
167  for i: U32
168  for v: U32
169  for h: {D.ok(b, d) == True{} : Bool}
170  {D.ok(B.set(b, i, v), d) == True{} : Bool}