def take_value

bendtorch-core@0.1.0.0 · src/tensor/slice_PROOF.bend:591

import Base
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
import bendtorch-core@0.1.0.0/src/tensor/slice.bend as Slice

591def take_value(-b: Array<F32>, pair: Array<F32> & F32) ->
592  {Pair.fst(F32, Array<F32> & Array<F32>, Slice.take(b, pair)) == Refinement.second(F32, pair) : F32}:
593  (a, x) = pair
594  {==}