def known_update
bendtorch-core@0.1.0.0 · src/tensor/core_PROOF.bend:418
import bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend as CorePROOF
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
418def known_update(-shape: Shape.Shape, -original: Core.Tensor<shape>, -output: Core.Tensor<shape>, +index: U32, +value: F32, -unit: Unit,
419 -exact: {(output, Done{unit}) == Core.write_flat(shape, original, index, value) : Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>},
420 certificate: Core.UpdateModel<shape, original, index, value>) -> KnownUpdate<shape, original, output, index, value, unit>:
421 Core.UpdateModel{meaning} = certificate
422 KnownUpdate{
423 %Equal.sym(Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>, (output, Done{unit}), Core.write_flat(shape, original, index, value), exact) :
424 Core.UpdateMeaning(shape, original, index, value, _)
425 meaning}