law to_list_view

lawful-bytes@0.1.1.0 · LAWS.bend:294

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

294law to_list_view:
295  for b: D.Bytes
296  for d: Nat
297  for s: U32
298  for n: U32
299  for h: {D.ok(b, d) == True{} : Bool}
300  for hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(b)) == True{} : Bool}
301  {Pair.snd(D.Bytes, List<&2, U32>, B.to_list(b, s, n)) == D.slice(D.view(b), U32.to_nat(s), U32.to_nat(n)) : List<&2, U32>}