def viewed_same

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

import Base
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

58def viewed_same(+kind: Gather.Lookup, +given: Slice.View, +count: Nat) ->
59  {Gather.viewed(kind, given, count) == Laws.viewed(kind, given, count) : Gather.Plan}:
60  Slice.View{+outer, +rows, +inner} = given
61  {==}