def words_naturals

bendtorch-core@0.1.0.0 · src/tensor/elementwise_PROOF.bend:503

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

503def words_naturals(+dimensions: List<&2, U32>) -> {Shape.words(Shape.naturals(dimensions)) == dimensions : List<&2, U32>}:
504  match dimensions:
505    case Nil{}:
506      {==}
507    case +head <> +tail:
508      %words_naturals(tail) : {U32.from_nat(U32.to_nat(head)) <> Shape.words(Shape.naturals(tail)) == head <> _ : List<&2, U32>}
509      %Conversion.word_natural_exact(head) : {U32.from_nat(U32.to_nat(head)) <> Shape.words(Shape.naturals(tail)) == _ <> Shape.words(Shape.naturals(tail)) : List<&2, U32>}
510      {==}