law of_list_ok

lawful-bytes@0.1.1.0 · LAWS.bend:287

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

287law of_list_ok:
288  for d: Nat
289  for xs: List<&2, U32>
290  for hd: {Nat.is_le(d, 29n) == True{} : Bool}
291  for hn: {Nat.is_le(List.length(&2, U32, xs), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
292  {D.ok(B.of_list(d, xs), d) == True{} : Bool}