~/jendhub

def ASet.side

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

import bend-ml-tensor-array@0.1.19.0/main.bend as BendMlTensorArray
import Base

2161def ASet.side(-T: Data, a: Array<T>, +n: U32, +k: U32, +w: Bool) -> ASet.Side(T, a, n, k, w):
2162  match a:
2163    case ALeaf{x}:
2164      ({==}, {==}, Unit{})
2165    case ANode{xs, ys}:
2166      # bend-lint: disable-next bend-lint-rules/performance/missed_fork -- a proof by one pass over the tree not-expected-because: proofs are checked, never run
2167      ASet.side_node(T, xs, ys, n, k, w, ASet.side(T, xs, U32.shr(n), k, U32.is_lt(k, U32.shr(U32.shr(n)))), ASet.side(T, ys, U32.shr(n), U32.sub(k, U32.shr(n)), U32.is_lt(U32.sub(k, U32.shr(n)), U32.shr(U32.shr(n)))))

Uses (10)

Used by (1)