def shaped_same

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

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

63def shaped_same(+plan: Gather.Plan, -dimensions: List<&2, U32>, built: Shape.ConstructResult<dimensions>) ->
64  {Gather.shaped(plan, dimensions, built) == Laws.output(dimensions, plan, built) : Result<&2, &2, Gather.Error, Gather.Planned>}:
65  match built:
66    case Shape.SError{error}:
67      {==}
68    case Shape.SBuilt{+shape, preserved}:
69      {==}