def swap_observed
bendtorch-core@0.1.0.0 · src/storage/refinement.bend:364
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
364def swap_observed(-T: Data, -d: Nat, -original: Array<T>, -i: U32, -new: T,
365 cert: SwapFull<T, d, original, i, new>) ->
366 {Some{second(T, Array.swap(T, original, i, new))} ==
367 Model.observe(T, d, original, route(d, i)) : Maybe<&2, T>}:
368 match cert:
369 case SwapFull{array, old, equal, written, observed, valid}:
370 %equal : {Some{second(T, _)} == Model.observe(T, d, original, route(d, i)) : Maybe<&2, T>}
371 observed