def take_state
bendtorch-core@0.1.0.0 · src/tensor/slice_PROOF.bend:596
import bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend as SlicePROOF
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
596def take_state(-b: Array<F32>, pair: Array<F32> & F32) ->
597 {Pair.snd(F32, Array<F32> & Array<F32>, Slice.take(b, pair)) == (Refinement.first(F32, pair), b) : Array<F32> & Array<F32>}:
598 (a, x) = pair
599 {==}