type MaskMode

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

import Base

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