GatherPROOF.accepted_taken: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend as GatherPROOF
Lines 71-84 of bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&start_line=71&end_line=84

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

# An accepted request's plan and output are what the laws name.
def accepted_taken(+kind: Gather.Lookup, +dimensions: List<&2, U32>, +at: Nat, +count: Nat) ->
  {Gather.accepted(kind, dimensions, at, count) == Laws.taken(kind, dimensions, at, count) : Result<&2, &2, Gather.Error, Gather.Planned>}:
  Equal.trans(Result<&2, &2, Gather.Error, Gather.Planned>, Gather.accepted(kind, dimensions, at, count),
    Gather.shaped(Laws.viewed(kind, Slice.sized(dimensions, at, Slice.holds_zero(dimensions)), count),
      Slice.resized(dimensions, at, U32.from_nat(count)), Shape.construct(Slice.resized(dimensions, at, U32.from_nat(count)))),
    Laws.taken(kind, dimensions, at, count),
    Equal.cong(Gather.Plan, Result<&2, &2, Gather.Error, Gather.Planned>,
      p => Gather.shaped(p, Slice.resized(dimensions, at, U32.from_nat(count)), Shape.construct(Slice.resized(dimensions, at, U32.from_nat(count)))),
      Gather.viewed(kind, Slice.sized(dimensions, at, Slice.holds_zero(dimensions)), count),
      Laws.viewed(kind, Slice.sized(dimensions, at, Slice.holds_zero(dimensions)), count),
      viewed_same(kind, Slice.sized(dimensions, at, Slice.holds_zero(dimensions)), count)),
    shaped_same(Laws.viewed(kind, Slice.sized(dimensions, at, Slice.holds_zero(dimensions)), count),
      Slice.resized(dimensions, at, U32.from_nat(count)), Shape.construct(Slice.resized(dimensions, at, U32.from_nat(count)))))

Uses (22):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=construct
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=Error
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=Lookup
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=Plan
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=Planned
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=accepted
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=shaped
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=viewed
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend&name=taken
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend&name=viewed
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&name=shaped_same
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&name=viewed_same
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice.bend&name=holds_zero
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice.bend&name=resized
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice.bend&name=sized