ElementwisePROOF.words_naturals: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend as ElementwisePROOF
Lines 503-510 of bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&start_line=503&end_line=510

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

def words_naturals(+dimensions: List<&2, U32>) -> {Shape.words(Shape.naturals(dimensions)) == dimensions : List<&2, U32>}:
  match dimensions:
    case Nil{}:
      {==}
    case +head <> +tail:
      %words_naturals(tail) : {U32.from_nat(U32.to_nat(head)) <> Shape.words(Shape.naturals(tail)) == head <> _ : List<&2, U32>}
      %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>}
      {==}

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=naturals
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=words
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend&name=word_natural_exact