def FillElements

bendtorch-core@0.1.0.0 · src/tensor/construction_PROOF.bend:157

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/construction_LAWS.bend as Laws

157def FillElements(-shape: Shape.Shape, +values: List<&2, F32>, +cursor: Nat, -tensor: Core.Tensor<shape>) -> Type:
158  @+index: U32 -> @+offset: Nat -> @at: {U32.to_nat(index) == Nat.add(cursor, offset) : Nat} ->
159    @inside: Shape.LT(offset, List.length(&2, F32, values)) ->
160      Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
161        {Core.checked_observe(shape, tensor, index) == Laws.list_element(values, offset) : Maybe<&2, F32>}