def word_equal

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

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

71def word_equal(+n: Nat, +a: Word(n), +b: Word(n),
72  +equal: {True{} == Layout.word_same(n, a, b) : Bool}) -> {a == b : Word(n)}:
73  match n:
74    case 0n:
75      match a b:
76        case WNil{} WNil{}:
77          {==}
78    case 1n++p:
79      WCon{+ab, +at} = a
80      WCon{+bb, +bt} = b
81      %bit_equal(ab, bb, Mapping.and_left(Bool.not(Bool.xor(ab, bb)), Layout.word_same(p, at, bt), equal)) :
82        {WCon{ab, at} == WCon{_, bt} : Word(1n+p)}
83      %word_equal(p, at, bt, Mapping.and_right(Bool.not(Bool.xor(ab, bb)), Layout.word_same(p, at, bt), equal)) :
84        {WCon{ab, at} == WCon{ab, _} : Word(1n+p)}
85      {==}