ReduceFiberProof.off_mask: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend as ReduceFiberProof
Lines 467-472 of bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&start_line=467&end_line=472

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape

def off_mask(+rest: List<&2, Shape.Row>, +left: Nat, +stride: Nat, +digit: Nat, +target: Nat, +mode: OffMode<rest, left, stride, digit, target>,
  +q: Nat, +below: {Nat.is_lt(q, stride) == True{} : Bool}) ->
  {False{} == Nat.is_eq(Nat.add(Nat.mul(left, digit), Shape.walk_left(rest, q)), target) : Bool}:
  Off{+bound, +differ} = mode
  Equal.sym(Bool, Nat.is_eq(Nat.add(Nat.mul(left, digit), Shape.walk_left(rest, q)), target), False{},
    mask_off(left, digit, Shape.walk_left(rest, q), target, bound_at(rest, left, stride, bound, q, below), differ))

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=OffMode
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=bound_at
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=mask_off
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Row
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=walk_left