def ASet.size_pair

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

import Base

1957# Array.size hands back the array it measured, next to ASet.sz(T, a)
1958def ASet.size_pair(-T: Data, a: Array<T>) -> {(a, ASet.sz(T, a)) == Array.size(T, a) : Array<T> & U32}:
1959  match a:
1960    case ALeaf{x}:
1961      {==}
1962    case ANode{xs, ys}:
1963      %ASet.size_pair(T, xs) : {(ANode{xs, ys}, Pair.snd(Array<T>, U32, Array.size.node(T, ys, _))) == Array.size.node(T, ys, _) : Array<T> & U32}
1964      {==}