def finish_write
bendtorch-core@0.1.0.0 · src/storage/main.bend:85
import bendtorch-core@0.1.0.0/src/storage/main.bend as BendtorchCore
import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/certificates.bend as Certificates
85def finish_write(+d: Nat, n: Nat, -original: Array<F32>, -i: U32, -value: F32,
86 array: Array<F32>, -exact: {array == Array.set(F32, original, i, value) : Array<F32>},
87 -balanced: Model.Balanced(F32, d, original), -valid: {bounds(d, n) == True{} : Bool}) ->
88 Storage & Result<&2, &2, Error, Unit>:
89 (Owned{d, n, array, Certificates.set_result(F32, d, original, i, value, array, exact, balanced), valid}, Done{Unit{}})