def block_off

bendtorch-core@0.1.0.0 · src/autograd/reduce_fiber_proof.bend:547

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend as Broadcast
import bendtorch-core@0.1.0.0/src/storage/api.bend as Api

547def block_off(+stride: Nat, +left: Nat, +right: Nat, +rest: List<&2, Shape.Row>, +target: Nat, +base: Nat, +digit: Nat,
548  +mode: OffMode<rest, left, stride, digit, target>) ->
549  {masked(stride, Shape.Row{stride, left, right} <> rest, target, base, Nat.mul(digit, stride)) == Nil{} : List<&2, Nat>}:
550  %Broadcast.add_zero(Nat.mul(digit, stride)) :
551    {masked(stride, Shape.Row{stride, left, right} <> rest, target, base, _) == Nil{} : List<&2, Nat>}
552  shifted_off(stride, stride, left, right, rest, target, base, digit, 0n, Api.le_refl(stride), mode)