ElementwiseWalkProof.walk_left_zero: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/elementwise_walk_proof.bend as ElementwiseWalkProof
Lines 125-134 of bendtorch-core@0.1.0.0/src/tensor/elementwise_walk_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_walk_proof.bend&start_line=125&end_line=134

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise

# Rows whose left stride is 0 on every axis: every position walks to 0.
def walk_left_zero(+rows: List<&2, Shape.Row>, +zero: {Elementwise.zero_left(rows) == True{} : Bool}, +i: Nat) ->
  {Shape.walk_left(rows, i) == 0n : Nat}:
  match rows:
    case Shape.Row{+stride, +left, +right} <> +rest:
      +none = Arith.eq_true(left, 0n, Arith.and_left(Nat.is_eq(left, 0n), Elementwise.zero_left(rest), zero))
      %Equal.sym(Nat, left, 0n, none) : {Nat.add(Nat.mul(_, Nat.div(i, stride)), Shape.walk_left(rest, Nat.mod(i, stride))) == 0n : Nat}
      walk_left_zero(rest, Arith.and_right(Nat.is_eq(left, 0n), Elementwise.zero_left(rest), zero), Nat.mod(i, stride))
    case Nil{}:
      {==}

Uses (15):
  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=List
  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.div
  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/shape/core.bend&name=Row
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=walk_left
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=and_left
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=and_right
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=eq_true
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=zero_left