def matches_others

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

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

45def matches_others(dimensions: List<&2, U32>, index: List<&2, U32>, +at: Nat) ->
46  {Gather.matches(dimensions, index, at) == Laws.others(dimensions, index, at) : Bool}:
47  match dimensions index at:
48    case x <> xs y <> ys 0n:
49      equal_same(xs, ys)
50    case +x <> xs +y <> ys 1n+next:
51      Equal.cong(Bool, Bool, b => Bool.and(Nat.is_eq(U32.to_nat(x), U32.to_nat(y)), b), Gather.matches(xs, ys, next), Laws.others(xs, ys, next),
52        matches_others(xs, ys, next))
53    case Nil{} index at:
54      {==}
55    case x <> xs Nil{} at:
56      {==}