def set_result

bendtorch-core@0.1.0.0 · src/storage/certificates.bend:13

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement

13def set_result(-T: Data, +d: Nat, original: Array<T>, +i: U32, +value: T, -result: Array<T>,
14  equal: {result == Array.set(T, original, i, value) : Array<T>},
15  valid: Model.Balanced(T, d, original)) -> Model.Balanced(T, d, result):
16  %Equal.sym(Array<T>, result, Array.set(T, original, i, value), equal) : Model.Balanced(T, d, _)
17  Refinement.law_set_balanced(T, d, original, i, value, valid)