def index_same

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

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
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

649def index_same(+entries: List<&2, U32>, -dimensions: List<&2, U32>, built: Shape.ConstructResult<dimensions>) ->
650  {Gather.built_index(entries, dimensions, built) == Laws.index_of(entries, dimensions, built) : Result<&2, &2, Gather.Error, Gather.Index>}:
651  match built:
652    case Shape.SError{error}:
653      {==}
654    case Shape.SBuilt{+shape, preserved}:
655      {==}