law cap_ok

bend-ml-tensor-array@0.1.19.0 · main.bend:736

import Base

736# LAW (cap_ok): an Array with 2^cap_depth(n) slots always has room for n elements.
737law cap_ok:
738  for +n: Nat
739  {True{} == leb(n, pow2(cap_depth(n))) : Bool}