def pad_strides

bendtorch-core@0.1.0.0 · src/shape/projection_proofs.bend:66

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

66def pad_strides(+count: Nat, +dims: List<&2, Nat>) -> {strides_of(Shape.pad(count, dims)) == zeros(count, strides_of(dims)) : List<&2, Nat>}:
67  match count:
68    case 0n:
69      {==}
70    case 1n+rest:
71      Equal.cong(List<&2, Nat>, List<&2, Nat>, tail => 0n <> tail, strides_of(Shape.pad(rest, dims)), zeros(rest, strides_of(dims)), pad_strides(rest, dims))