ReadWriteRecords.ReadInside: type of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/read_write_records.bend as ReadWriteRecords
Lines 15-18 of bendtorch-core@0.1.0.0/src/tensor/read_write_records.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/read_write_records.bend&start_line=15&end_line=18

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Observation

type ReadInside<-shape: Shape.Shape, -fill: F32, -index: U32> is Type:
  ReadInside{
    read: ReadContract<shape, fill, index, 0>,
    value: {Observation.point(shape, index, Core.new(shape, fill)) == Some{fill} : Maybe<&2, F32>}}

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  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=Shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=new
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/observation.bend&name=point
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/read_write_records.bend&name=ReadContract