PermutationMapping.words_same_refl: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/permutation_mapping.bend as PermutationMapping
Lines 561-568 of bendtorch-core@0.1.0.0/src/tensor/permutation_mapping.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/permutation_mapping.bend&start_line=561&end_line=568

import Base
import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout

def words_same_refl(+values: List<&2, U32>) -> {Layout.words_same(values, values) == True{} : Bool}:
  match values:
    case Nil{}:
      {==}
    case +head <> +tail:
      %Equal.sym(Bool, Layout.word_value_same(head, head), True{}, word_value_same_refl(head)) :
        {Bool.and(_, Layout.words_same(tail, tail)) == True{} : Bool}
      words_same_refl(tail)

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  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=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=word_value_same
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=words_same
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permutation_mapping.bend&name=word_value_same_refl