law push_ok

lawful-bytes@0.1.1.0 · LAWS.bend:181

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

181law push_ok:
182  for b: D.Bytes
183  for d: Nat
184  for v: U32
185  for h: {D.ok(b, d) == True{} : Bool}
186  for hc: {Nat.is_lt(D.size(b), D.cap(b)) == True{} : Bool}
187  {D.ok(B.push(b, v), d) == True{} : Bool}