ProjectionProofs.dot_zeros: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend as ProjectionProofs
Lines 73-85 of bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend&start_line=73&end_line=85

import Base
import bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend as Broadcast

def dot_zeros(+count: Nat, +values: List<&2, Nat>, +steps: List<&2, Nat>) -> {dot(zeros(count, steps), values) == dot(steps, List.drop(&2, Nat, values, count)) : Nat}:
  match count values:
    case 0n values:
      %Broadcast.drop_zero(values) : {dot(steps, values) == dot(steps, _) : Nat}
      {==}
    case 1n+rest Nil{}:
      match steps:
        case Nil{}:
          {==}
        case head <> tail:
          {==}
    case 1n+rest +value <> +tail:
      dot_zeros(rest, tail, steps)

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.drop
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend&name=drop_zero
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend&name=dot
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend&name=zeros