law size_count

lawful-arrays@0.1.0.0 · LAWS.bend:39

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

39# Array.size doubles 1 once per level of the left spine: for a perfect tree of
40# depth d below 32 that is the number of leaves, 2^d.
41law size_count:
42  for -T: Data
43  for a: Array<T>
44  for d: Nat
45  for hf: {D.full(T, a, d) == True{} : Bool}
46  for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
47  {U32.to_nat(Pair.snd(Array<T>, U32, Array.size(T, a))) == Nat.pow(2n, d) : Nat}