type Written

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

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

181type Written<-shape: Shape.Shape, -original: Core.Tensor<shape>, -tensor: Core.Tensor<shape>, -cursor: Nat, -value: F32> is Data:
182  Written{-point: @+index: U32 -> @at: {U32.to_nat(index) == cursor : Nat} ->
183      Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
184        {Core.checked_observe(shape, tensor, index) == Some{value} : Maybe<&2, F32>},
185    -frame: FillFrame(shape, original, cursor, tensor)}