def source_word

bendtorch-core@0.1.0.0 · src/tensor/permute_build_proof.bend:170

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Values
import bendtorch-core@0.1.0.0/src/tensor/permute_build.bend as Build

170# The word index a cell reads is `permute_source_index` as a word.
171def source_word(+input: Shape.Shape, +axes: List<&2, U32>, +index: Nat) ->
172  {Build.at(Build.recipe(Build.Request{input, axes}), index) == U32.from_nat(Values.permute_source_index(input, axes, index)) : U32}:
173  Equal.cong(Nat, U32, number => U32.from_nat(number), Build.source(Build.recipe(Build.Request{input, axes}), index),
174    Values.permute_source_index(input, axes, index), source_index(input, axes, index))