def take_snd
bendtorch-core@0.1.0.0 · src/tensor/gather_PROOF.bend:238
import bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend as GatherPROOF
import Base
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
import bendtorch-core@0.1.0.0/src/tensor/gather.bend as Gather
238def take_snd(index: Array<U32>, pair: Array<F32> & F32) ->
239 {Pair.snd(F32, Array<F32> & Array<U32>, Gather.take(index, pair)) == (Refinement.first(F32, pair), index) : Array<F32> & Array<U32>}:
240 (a, x) = pair
241 {==}