ReduceFiberProof.mode_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 452-462 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=452&end_line=462

import Base

def mode_mask(+left: Nat, +digit: Nat, +target: Nat, +inner: Nat, +mode: MaskMode<left, digit, target, inner>, +w: Nat) ->
  {Nat.is_eq(w, inner) == Nat.is_eq(Nat.add(Nat.mul(left, digit), w), target) : Bool}:
  match mode:
    case Free{zero, same}:
      %zero : {Nat.is_eq(w, inner) == Nat.is_eq(Nat.add(Nat.mul(_, digit), w), target) : Bool}
      %Equal.sym(Nat, target, inner, same) : {Nat.is_eq(w, inner) == Nat.is_eq(w, _) : Bool}
      {==}
    case Hit{given, same, remainder}:
      %remainder : {Nat.is_eq(w, _) == Nat.is_eq(Nat.add(Nat.mul(left, digit), w), target) : Bool}
      Equal.sym(Bool, Nat.is_eq(Nat.add(Nat.mul(left, digit), w), target), Nat.is_eq(w, Nat.mod(target, left)),
        mask_at(left, digit, w, target, given, same))

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=Equal.sym
  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.mod
  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=MaskMode
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=mask_at