law size_pair

lawful-arrays@0.1.0.0 · LAWS.bend:177

import Base
import lawful-arrays@0.1.0.0/defs.bend as D

177law size_pair:
178  for -T: Data
179  for a: Array<T>
180  for d: Nat
181  for hf: {D.full(T, a, d) == True{} : Bool}
182  {Array.size(T, a) == (a, U32.shln(1, d)) : Array<T> & U32}