def mode_mask

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

import Base

452def mode_mask(+left: Nat, +digit: Nat, +target: Nat, +inner: Nat, +mode: MaskMode<left, digit, target, inner>, +w: Nat) ->
453  {Nat.is_eq(w, inner) == Nat.is_eq(Nat.add(Nat.mul(left, digit), w), target) : Bool}:
454  match mode:
455    case Free{zero, same}:
456      %zero : {Nat.is_eq(w, inner) == Nat.is_eq(Nat.add(Nat.mul(_, digit), w), target) : Bool}
457      %Equal.sym(Nat, target, inner, same) : {Nat.is_eq(w, inner) == Nat.is_eq(w, _) : Bool}
458      {==}
459    case Hit{given, same, remainder}:
460      %remainder : {Nat.is_eq(w, _) == Nat.is_eq(Nat.add(Nat.mul(left, digit), w), target) : Bool}
461      Equal.sym(Bool, Nat.is_eq(Nat.add(Nat.mul(left, digit), w), target), Nat.is_eq(w, Nat.mod(target, left)),
462        mask_at(left, digit, w, target, given, same))