def known_checked_update
bendtorch-core@0.1.0.0 · src/tensor/transform_PROOF.bend:468
import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformPROOF
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
468def known_checked_update(-shape: Shape.Shape, -original: Core.Tensor<shape>, -output: Core.Tensor<shape>, +index: U32,
469 +value: F32, -unit: Unit,
470 -exact: {(output, Done{unit}) == Core.write_flat(shape, original, index, value) : Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>},
471 certificate: Core.CheckedUpdateModel<shape, original, index, value>) -> KnownCheckedUpdate<shape, original, output, index, value, unit>:
472 Core.CheckedUpdateModel{meaning} = certificate
473 KnownCheckedUpdate{
474 %Equal.sym(Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>, (output, Done{unit}), Core.write_flat(shape, original, index, value), exact) :
475 Core.CheckedUpdateMeaning(shape, original, index, value, _)
476 meaning}