law primitive_update_frame

bendtorch-core@0.1.0.0 · src/storage/LAWS.bend:42

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

42law primitive_update_frame:
43  for -T: Data
44  for +d: Nat
45  for array: Array<T>
46  for +i: U32
47  for +other: Model.Path(d)
48  for +value: T
49  for valid: Model.Balanced(T, d, array)
50  {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>}