def primitive_update_frame

bendtorch-core@0.1.0.0 · src/storage/frame.bend:94

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
import bendtorch-core@0.1.0.0/src/storage/clone.bend as Clone

94def primitive_update_frame(-T: Data, +d: Nat, array: Array<T>, +i: U32, +other: Model.Path(d), +value: T, valid: Model.Balanced(T, d, array)) ->
95  {Model.observe(T, d, Array.set(T, array, i, value), other) == Model.select(T, Model.same(d, Refinement.route(d, i), other), value, Model.observe(T, d, array, other)) : Maybe<&2, T>}:
96  primitive_frame_cloned(T, d, array, i, other, value, Clone.certify(T, d, array, valid))