def located_index
bendtorch-core@0.1.0.0 · src/tensor/write_contract.bend:133
import bendtorch-core@0.1.0.0/src/tensor/write_contract.bend as WriteContract
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 Observation
133def located_index(-shape: Shape.Shape, +index: Shape.FlatIndex<shape>, +expected: U32,
134 located: {Observation.coordinate_index(shape, Done{index}) == Some{expected} : Maybe<&2, U32>}) ->
135 {Shape.index_value(shape, index) == expected : U32}:
136 Equal.cong(Maybe<&2, U32>, U32, word => Maybe.default(&2, U32, word, 0), Some{Shape.index_value(shape, index)}, Some{expected}, located)