def equal_same

bendtorch-core@0.1.0.0 · src/tensor/gather_PROOF.bend:33

import Base
import bendtorch-core@0.1.0.0/src/tensor/gather.bend as Gather
import bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend as Laws

33def equal_same(left: List<&2, U32>, right: List<&2, U32>) -> {Gather.equal(left, right) == Laws.equal(left, right) : Bool}:
34  match left right:
35    case Nil{} Nil{}:
36      {==}
37    case +x <> xs +y <> ys:
38      Equal.cong(Bool, Bool, b => Bool.and(Nat.is_eq(U32.to_nat(x), U32.to_nat(y)), b), Gather.equal(xs, ys), Laws.equal(xs, ys),
39        equal_same(xs, ys))
40    case Nil{} y <> ys:
41      {==}
42    case x <> xs Nil{}:
43      {==}