law size_perfect

bend-osdev-array@0.1.0.1 · LAWS.bend:72

import Base
import bend-osdev-array@0.1.0.1/array.bend as A

72law size_perfect:
73  for -T: Data
74  for d: Nat
75  for a: Array<T>
76  for h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}
77  {Array.size(T, a) == (a, U32.shln(1, d)) : Array<T> & U32}