~/jendhub

def brow

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

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

1748# row i; left says whether i is in the first band of the node (i < half(rr))
1749def brow(+c: Nat, -r: Nat, b: Bands<r, c>, left: Bool, +rr: Nat, -e: {rr == r : Nat}, +i: Nat) -> BRow<r, c>:
1750  match b left:
1751    case BLeaf{m} _:
1752      brow_leaf(r, c, m, U32.from_nat(Nat.mul(i, c)), c)
1753    case BNode{x, y} True{}:
1754      brow_l(r, c, brow(c, half(r), x, Nat.is_lt(i, half(half(rr))), half(rr), eq_half(rr, r, e), i), y)
1755    case BNode{x, y} False{}:
1756      brow_r(r, c, x, brow(c, Nat.sub(r, half(r)), y, Nat.is_lt(Nat.sub(i, half(rr)), half(Nat.sub(rr, half(rr)))), Nat.sub(rr, half(rr)), eq_rest(rr, r, e), Nat.sub(i, half(rr))))

Uses (14)

Used by (1)