def finish_read
bendtorch-core@0.1.0.0 · src/storage/main.bend:61
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
61def finish_read(+d: Nat, n: Nat, -original: Array<F32>, -i: U32,
62 result: Array<F32> & F32, -exact: {result == Array.get(F32, original, i) : Array<F32> & F32},
63 -balanced: Model.Balanced(F32, d, original), -valid: {bounds(d, n) == True{} : Bool}) ->
64 Storage & Result<&2, &2, Error, F32>:
65 (array, value) = result
66 (Owned{d, n, array, Certificates.get_result(F32, d, original, i, (array, value), exact, balanced), valid}, Done{value})