def words_naturals

bendtorch-core@0.1.0.0 · src/tensor/transform_PROOF.bend:1726

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

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