def mul_zero_factor

bendtorch-core@0.1.0.0 · src/tensor/slice_PROOF.bend:407

import Base
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

407def mul_zero_factor(+a: Nat, +b: Nat, e: {Nat.mul(a, b) == 0n : Nat}, nonzero: {False{} == Nat.is_eq(a, 0n) : Bool}) -> {b == 0n : Nat}:
408  match a:
409    case 0n:
410      Empty.absurd({b == 0n : Nat}, Arith.clash(nonzero))
411    case 1n+p:
412      add_zero_left_part(b, Nat.mul(p, b), e)