BroadcastProofs.drop_broadcast: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend as BroadcastProofs
Lines 194-205 of bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend&start_line=194&end_line=205

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

def drop_broadcast(+count: Nat, +dims: List<&2, Nat>, +values: List<&2, Nat>) -> {List.drop(&2, Nat, Shape.broadcast_indices(Shape.pad(count, dims), values), count) == Shape.broadcast_indices(dims, List.drop(&2, Nat, values, count)) : List<&2, Nat>}:
  match count:
    case 0n:
      %drop_zero(values) : {List.drop(&2, Nat, Shape.broadcast_indices(dims, values), 0n) == Shape.broadcast_indices(dims, _) : List<&2, Nat>}
      %drop_zero(Shape.broadcast_indices(dims, values)) : {_ == Shape.broadcast_indices(dims, values) : List<&2, Nat>}
      {==}
    case 1n+rest:
      match values:
        case Nil{}:
          broadcast_nil(dims)
        case +head <> +tail:
          drop_broadcast(rest, dims, tail)

Uses (7):
  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=broadcast_nil
  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/core.bend&name=broadcast_indices
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=pad