law capacity_view

lawful-bytes@0.1.1.0 · LAWS.bend:233

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

233law capacity_view:
234  for b: D.Bytes
235  for d: Nat
236  for h: {D.ok(b, d) == True{} : Bool}
237  {U32.to_nat(Pair.snd(D.Bytes, U32, B.capacity(b))) == D.cap(b) : Nat}