TransformPROOF.words_equal: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformPROOF
Lines 92-106 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=92&end_line=106

import Base
import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
import bendtorch-core@0.1.0.0/src/tensor/permutation_mapping.bend as Mapping

def words_equal(+a: List<&2, U32>, +b: List<&2, U32>,
  +equal: {True{} == Layout.words_same(a, b) : Bool}) -> {a == b : List<&2, U32>}:
  match a b:
    case Nil{} Nil{}:
      {==}
    case +ah <> +at +bh <> +bt:
      %word_value_equal(ah, bh, Mapping.and_left(Layout.word_value_same(ah, bh), Layout.words_same(at, bt), equal)) :
        {ah <> at == _ <> bt : List<&2, U32>}
      %words_equal(at, bt, Mapping.and_right(Layout.word_value_same(ah, bh), Layout.words_same(at, bt), equal)) :
        {ah <> at == ah <> _ : List<&2, U32>}
      {==}
    case Nil{} bh <> bt:
      Empty.absurd({Nil{} == bh <> bt : List<&2, U32>}, Lifecycle.false_true(equal))
    case ah <> at Nil{}:
      Empty.absurd({ah <> at == Nil{} : List<&2, U32>}, Lifecycle.false_true(equal))

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  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/lifecycle.bend&name=false_true
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permutation_mapping.bend&name=and_left
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permutation_mapping.bend&name=and_right
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=word_value_equal