def mask_off_decided

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

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

206def mask_off_decided(+size: Nat, +d: Nat, +w: Nat, +t: Nat, below: {Nat.is_lt(w, size) == True{} : Bool},
207  differ: {Nat.is_eq(d, Nat.div(t, size)) == False{} : Bool},
208  decision: Shape.BoolCase<Nat.is_eq(Nat.add(Nat.mul(size, d), w), t)>) ->
209  {Nat.is_eq(Nat.add(Nat.mul(size, d), w), t) == False{} : Bool}:
210  match decision:
211    case Shape.BFalse{equal}:
212      Equal.sym(Bool, False{}, Nat.is_eq(Nat.add(Nat.mul(size, d), w), t), equal)
213    case Shape.BTrue{equal}:
214      +hit = Arith.eq_true(Nat.add(Nat.mul(size, d), w), t, Equal.sym(Bool, True{}, Nat.is_eq(Nat.add(Nat.mul(size, d), w), t), equal))
215      Empty.absurd({Nat.is_eq(Nat.add(Nat.mul(size, d), w), t) == False{} : Bool},
216        ne_from(d, Nat.div(t, size),
217          div_of(t, size, d, w, below,
218            %Nats.mul_comm(size, d) : {Nat.add(_, w) == t : Nat}
219            hit),
220          differ))