def ASet.facts
bend-ml-tensor-array@0.1.19.0 · main.bend:1996
import bend-ml-tensor-array@0.1.19.0/main.bend as BendMlTensorArray
import Base
1996def ASet.facts(-T: Data, a: Array<T>, +n: U32, +j: U32, +v: T, +z: Bool) -> ASet.Facts(T, a, n, j, v, z):
1997 match a z:
1998 case ALeaf{x} _:
1999 ({==}, {==}, {==}, {==}, {==}, {==}, Unit{})
2000 case ANode{xs, ys} True{}:
2001 ASet.node_t(T, xs, ys, n, j, v, ASet.facts(T, xs, U32.shr(n), j, v, U32.is_lt(j, U32.shr(U32.shr(n)))))
2002 case ANode{xs, ys} False{}:
2003 ASet.node_f(T, xs, ys, n, j, v, ASet.size_pair(T, xs), ASet.facts(T, ys, U32.shr(n), U32.sub(j, U32.shr(n)), v, U32.is_lt(U32.sub(j, U32.shr(n)), U32.shr(U32.shr(n)))))