def extent

bendtorch-core@0.1.0.0 · src/storage/size.bend:50

import Base

50def extent(-T: Data, -d: Nat, -original: Array<T>, sized: Sized<T, d, original>) ->
51  {Pair.snd(Array<T>, U32, Array.size(T, original)) == capacity(d) : U32}:
52  match sized:
53    case Sized{array, n, retained, measured, extent, balanced}:
54      Equal.trans(U32, Pair.snd(Array<T>, U32, Array.size(T, original)), n, capacity(d),
55        Equal.cong(Array<T> & U32, U32, r => Pair.snd(Array<T>, U32, r),
56          Array.size(T, original), (array, n),
57          Equal.sym(Array<T> & U32, (array, n), Array.size(T, original), measured)), extent)