def words_equal

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

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

92def words_equal(+a: List<&2, U32>, +b: List<&2, U32>,
93  +equal: {True{} == Layout.words_same(a, b) : Bool}) -> {a == b : List<&2, U32>}:
94  match a b:
95    case Nil{} Nil{}:
96      {==}
97    case +ah <> +at +bh <> +bt:
98      %word_value_equal(ah, bh, Mapping.and_left(Layout.word_value_same(ah, bh), Layout.words_same(at, bt), equal)) :
99        {ah <> at == _ <> bt : List<&2, U32>}
100      %words_equal(at, bt, Mapping.and_right(Layout.word_value_same(ah, bh), Layout.words_same(at, bt), equal)) :
101        {ah <> at == ah <> _ : List<&2, U32>}
102      {==}
103    case Nil{} bh <> bt:
104      Empty.absurd({Nil{} == bh <> bt : List<&2, U32>}, Lifecycle.false_true(equal))
105    case ah <> at Nil{}:
106      Empty.absurd({ah <> at == Nil{} : List<&2, U32>}, Lifecycle.false_true(equal))