law push_view

lawful-bytes@0.1.1.0 · LAWS.bend:172

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

172law push_view:
173  for b: D.Bytes
174  for d: Nat
175  for v: U32
176  for h: {D.ok(b, d) == True{} : Bool}
177  for hc: {Nat.is_lt(D.size(b), D.cap(b)) == True{} : Bool}
178  for hv: {U32.is_lt(v, 256) == True{} : Bool}
179  {D.view(B.push(b, v)) == List.append(&2, U32, D.view(b), [v]) : List<&2, U32>}