def others

bendtorch-core@0.1.0.0 · src/tensor/gather_LAWS.bend:57

import Base

57# Whether a gather index has the input's extent at every axis but `at`.
58def others(dimensions: List<&2, U32>, index: List<&2, U32>, +at: Nat) -> Bool:
59  match dimensions index at:
60    case x <> xs y <> ys 0n:
61      equal(xs, ys)
62    case x <> xs y <> ys 1n+next:
63      Bool.and(Nat.is_eq(U32.to_nat(x), U32.to_nat(y)), others(xs, ys, next))
64    case _ _ _:
65      False{}