law view_size

lawful-bytes@0.1.1.0 · LAWS.bend:15

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

15law view_size:
16  for b: D.Bytes
17  for d: Nat
18  for h: {D.ok(b, d) == True{} : Bool}
19  {List.length(&2, U32, D.view(b)) == D.size(b) : Nat}