def retains

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

import Base

41def retains(-T: Data, -d: Nat, -original: Array<T>, sized: Sized<T, d, original>) ->
42  {Pair.fst(Array<T>, U32, Array.size(T, original)) == original : Array<T>}:
43  match sized:
44    case Sized{array, n, retained, measured, extent, balanced}:
45      Equal.trans(Array<T>, Pair.fst(Array<T>, U32, Array.size(T, original)), array, original,
46        Equal.cong(Array<T> & U32, Array<T>, r => Pair.fst(Array<T>, U32, r),
47          Array.size(T, original), (array, n),
48          Equal.sym(Array<T> & U32, (array, n), Array.size(T, original), measured)), retained)