def take_fst

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

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

243def take_fst(index: Array<U32>, pair: Array<F32> & F32) ->
244  {Pair.fst(F32, Array<F32> & Array<U32>, Gather.take(index, pair)) == Refinement.second(F32, pair) : F32}:
245  (a, x) = pair
246  {==}