law truncate_ok

lawful-bytes@0.1.1.0 · LAWS.bend:249

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

249law truncate_ok:
250  for b: D.Bytes
251  for d: Nat
252  for n: U32
253  for h: {D.ok(b, d) == True{} : Bool}
254  for hn: {Nat.is_le(U32.to_nat(n), D.size(b)) == True{} : Bool}
255  {D.ok(B.truncate(b, n), d) == True{} : Bool}