ReadContract.read_contract: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/tensor/read_contract.bend as ReadContract Lines 196-209 of bendtorch-core@0.1.0.0/src/tensor/read_contract.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/read_contract.bend&start_line=196&end_line=209 import Base import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws 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 import bendtorch-core@0.1.0.0/src/tensor/read_write_records.bend as Laws def read_contract(+shape: Shape.Shape, +fill: F32, +index: U32, -expected: Result<&2, &2, Storage.Error, F32>, read: {StorageLaws.read(StorageLaws.created(Shape.count(shape), fill), index) == expected : Result<&2, &2, Storage.Error, F32>}) -> Laws.ReadContract: Laws.ReadContract{ new_lift(shape, fill, result => {Observation.read_code(shape, index, result) == Some{Observation.read_status(Core.storage_read_error(expected))} : Maybe<&2, U32>}, valid => read_code_done(shape, fill, valid, index, expected, read)), new_lift(shape, fill, result => {Observation.after_dimensions(shape, index, result) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>}, valid => read_dimensions_pair(shape, Core.read_flat(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}, index))), new_lift(shape, fill, result => {Observation.after_length(shape, index, result) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}, valid => read_length_done(shape, fill, valid, index)), new_lift(shape, fill, result => {Observation.after_count(shape, index, result) == Some{Shape.count(shape)} : Maybe<&2, U32>}, valid => read_count_pair(shape, Core.read_flat(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}, index))), other => inside => new_lift(shape, fill, result => {Observation.after_value(shape, index, other, result) == Some{fill} : Maybe<&2, F32>}, valid => read_after_done(shape, fill, valid, index, other, inside))} Uses (29): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat 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=Shape https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=count https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=dimensions https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=logical_numel https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=created https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=read https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=Error https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Tensor https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=read_flat https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=storage_read_error https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/observation.bend&name=after_count https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/observation.bend&name=after_dimensions https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/observation.bend&name=after_length https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/observation.bend&name=after_value https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/observation.bend&name=read_code https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/observation.bend&name=read_status https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/read_contract.bend&name=new_lift https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/read_contract.bend&name=read_after_done https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/read_contract.bend&name=read_code_done https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/read_contract.bend&name=read_count_pair https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/read_contract.bend&name=read_dimensions_pair https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/read_contract.bend&name=read_length_done https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/read_write_records.bend&name=ReadContract