def pad_length

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

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

140def pad_length(+count: Nat, +dims: List<&2, Nat>) -> {Nat.add(count, List.length(&2, Nat, dims)) == List.length(&2, Nat, Shape.pad(count, dims)) : Nat}:
141  match count:
142    case 0n:
143      {==}
144    case 1n+rest:
145      %pad_length(rest, dims) : {1n+Nat.add(rest, List.length(&2, Nat, dims)) == 1n+_ : Nat}
146      {==}