def unpad_indices

bendtorch-core@0.1.0.0 · src/shape/broadcast_proofs.bend:207

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

207def unpad_indices(+count: Nat, +dims: List<&2, Nat>, +coordinate: Shape.Coordinate(Shape.pad(count, dims))) -> {Shape.indices(dims, Shape.unpad(count, dims, coordinate)) == List.drop(&2, Nat, Shape.indices(Shape.pad(count, dims), coordinate), count) : List<&2, Nat>}:
208  match count:
209    case 0n:
210      drop_zero(Shape.indices(dims, coordinate))
211    case 1n+rest:
212      Shape.CStep{index, +tail} = coordinate
213      unpad_indices(rest, dims, tail)