TransformPROOF.words_naturals: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformPROOF
Lines 1726-1733 of bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&start_line=1726&end_line=1733

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 WordConversion

def words_naturals(+values: List<&2, U32>) -> {Shape.words(Shape.naturals(values)) == values : List<&2, U32>}:
  match values:
    case Nil{}:
      {==}
    case +head <> +tail:
      %Equal.sym(U32, U32.from_nat(U32.to_nat(head)), head, WordConversion.word_natural_exact(head)) :
        {_ <> Shape.words(Shape.naturals(tail)) == head <> tail : List<&2, U32>}
      Equal.cong(List<&2, U32>, List<&2, U32>, rest => head <> rest, Shape.words(Shape.naturals(tail)), tail, words_naturals(tail))

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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