ReduceFiberProof.mask_off: 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 222-225 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=222&end_line=225

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

def mask_off(+size: Nat, +d: Nat, +w: Nat, +t: Nat, below: {Nat.is_lt(w, size) == True{} : Bool},
  differ: {Nat.is_eq(d, Nat.div(t, size)) == False{} : Bool}) ->
  {Nat.is_eq(Nat.add(Nat.mul(size, d), w), t) == False{} : Bool}:
  mask_off_decided(size, d, w, t, below, differ, Shape.bool_case(Nat.is_eq(Nat.add(Nat.mul(size, d), w), t)))

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.div
  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=mask_off_decided
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=bool_case