def naturals_pad

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

import Base

791def naturals_pad(+count: Nat, -dims: List<&2, U32>) -> {naturals(pad_words(count, dims)) == pad(count, naturals(dims)) : List<&2, Nat>}:
792  match count:
793    case 0n:
794      {==}
795    case 1n+rest:
796      %naturals_pad(rest, dims) : {1n <> naturals(pad_words(rest, dims)) == 1n <> _ : List<&2, Nat>}
797      {==}