WriteContract.located_index: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/write_contract.bend as WriteContract
Lines 133-136 of bendtorch-core@0.1.0.0/src/tensor/write_contract.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/write_contract.bend&start_line=133&end_line=136

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

def located_index(-shape: Shape.Shape, +index: Shape.FlatIndex<shape>, +expected: U32,
  located: {Observation.coordinate_index(shape, Done{index}) == Some{expected} : Maybe<&2, U32>}) ->
  {Shape.index_value(shape, index) == expected : U32}:
  Equal.cong(Maybe<&2, U32>, U32, word => Maybe.default(&2, U32, word, 0), Some{Shape.index_value(shape, index)}, Some{expected}, located)

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe.default
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=FlatIndex
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=index_value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/observation.bend&name=coordinate_index