FromValuesContract.from_values_contract: 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 357-377 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=357&end_line=377

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
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/allocation_spec.bend as Allocation
import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Observation
import bendtorch-core@0.1.0.0/src/tensor/from_values_records.bend as Laws

def from_values_contract(+shape: Shape.Shape, +values: List<&2, F32>,
  counted: {List.length(&2, F32, values) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
  Laws.FromValuesContract<shape, values>:
  +counted = counted
  Laws.FromValuesContract{
    from_values_lift(shape, values, counted,
      result => {Result.is_done(&2, &1, Core.Error, Core.Tensor<shape>, result) == True{} : Bool}, fits => {==}),
    from_values_lift(shape, values, counted,
      result => {Observation.dimensions(shape, result) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>}, fits => {==}),
    from_values_lift(shape, values, counted,
      result => {Allocation.tensor_length(shape, result) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>},
      fits => Equal.cong(Nat, Maybe<&2, Nat>, number => Some{number},
        Lifecycle.logical_length(StorageLaws.replay(writes(values, 0n), base(shape, Nil{}))), Shape.logical_numel(Shape.dimensions(shape)),
        filled_length(shape, values))),
    from_values_lift(shape, values, counted,
      result => {Observation.count(shape, result) == Some{Shape.count(shape)} : Maybe<&2, U32>}, fits => {==}),
    index => inside =>
      +inside = inside
      from_values_lift(shape, values, counted,
        result => {Observation.point(shape, index, result) == List.get(&2, F32, values, U32.to_nat(index)) : Maybe<&2, F32>},
        fits => filled_value(shape, values, counted, index, inside, fits))}

Uses (29):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  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=Result.is_done
  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=replay
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/allocation_spec.bend&name=tensor_length
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.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/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=filled_length
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/from_values_contract.bend&name=filled_value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/from_values_contract.bend&name=from_values_lift
  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_records.bend&name=FromValuesContract
  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/observation.bend&name=count
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/observation.bend&name=dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/observation.bend&name=point