ReduceFiberProof.MaskMode: type of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend as ReduceFiberProof
Lines 444-450 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=444&end_line=450

import Base

# How the rows below a block decide which positions land on the target: on
# a reduced row (left stride 0) the rows below land on the target itself; on
# the kept row's target digit they land on the target's remainder; on any
# other digit of a kept row nothing lands.
type MaskMode<-left: Nat, -digit: Nat, -target: Nat, -inner: Nat> is Data:
  Free{zero: {0n == left : Nat}, same: {target == inner : Nat}}
  Hit{given: Decomposed<target, left>, same: {digit == Nat.div(target, left) : Nat}, remainder: {Nat.mod(target, left) == inner : Nat}}

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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.mod
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=Decomposed