FromValuesContract.filled_value: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/from_values_contract.bend as FromValuesContract
Lines 332-355 of bendtorch-core@0.1.0.0/src/tensor/from_values_contract.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/from_values_contract.bend&start_line=332&end_line=355

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/lifecycle.bend as Lifecycle
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Observation
import bendtorch-core@0.1.0.0/src/tensor/read_contract.bend as Reads

def filled_value(+shape: Shape.Shape, +values: List<&2, F32>,
  +counted: {List.length(&2, F32, values) == Shape.logical_numel(Shape.dimensions(shape)) : Nat},
  +index: U32, +inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool},
  -fits: {Lifecycle.logical_length(StorageLaws.replay(writes(values, 0n), base(shape, Nil{}))) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
  {Observation.point(shape, index, Done{Core.TTensor{StorageLaws.replay(writes(values, 0n), base(shape, Nil{})), fits}}) ==
    List.get(&2, F32, values, U32.to_nat(index)) : Maybe<&2, F32>}:
  Equal.trans(Maybe<&2, F32>,
    Observation.point(shape, index, Done{Core.TTensor{StorageLaws.replay(writes(values, 0n), base(shape, Nil{})), fits}}),
    Lifecycle.read_value(Storage.get(StorageLaws.replay(writes(values, 0n), base(shape, Nil{})), index)),
    List.get(&2, F32, values, U32.to_nat(index)),
    Core.read_result_value(shape, StorageLaws.replay(writes(values, 0n), base(shape, Nil{})), fits, index,
      Storage.get(StorageLaws.replay(writes(values, 0n), base(shape, Nil{})), index), {==}),
    Equal.trans(Maybe<&2, F32>,
      Lifecycle.read_value(Storage.get(StorageLaws.replay(writes(values, 0n), base(shape, Nil{})), index)),
      Some{StorageLaws.expected(writes(values, 0n), U32.to_nat(Shape.count(shape)), index, 0.0)},
      List.get(&2, F32, values, U32.to_nat(index)),
      Reads.stored_value(StorageLaws.replay(writes(values, 0n), base(shape, Nil{})), index,
        StorageLaws.expected(writes(values, 0n), U32.to_nat(Shape.count(shape)), index, 0.0),
        StorageLaws.replay_get(Shape.count(shape), 0.0, writes(values, 0n), index, Conversion.shape_count_within(shape),
          Reads.word_inside(shape, index, inside))),
      written_at(values, 0n, Shape.count(shape), index, 0.0, U32.to_nat(index), start_room(shape, values, counted), {==},
        %Equal.sym(Nat, List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape)), counted) :
          {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
        inside)))

Uses (33):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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=List.get
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  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=Nat.is_lt
  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=Base/base.bend&name=U32.to_nat
  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=expected
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=replay
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=replay_get
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=get
  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_result_value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/from_values_contract.bend&name=base
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/from_values_contract.bend&name=start_room
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/from_values_contract.bend&name=writes
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/from_values_contract.bend&name=written_at
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend&name=logical_length
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend&name=read_value
  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_contract.bend&name=stored_value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/read_contract.bend&name=word_inside
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend&name=shape_count_within