def observed_transport

bendtorch-core@0.1.0.0 · src/storage/refinement.bend:233

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/size.bend as Size

233def observed_transport(-T: Data, -d: Nat, -array: Array<T>, -original: Array<T>,
234  -n: U32, -i: U32, -value: T,
235  kept: {array == original : Array<T>}, extent: {n == Size.capacity(d) : U32},
236  observed: {Some{value} == Model.observe(T, d, array, route_n(d, n, i)) : Maybe<&2, T>}) ->
237  {Some{value} == Model.observe(T, d, original, route(d, i)) : Maybe<&2, T>}:
238  %kept : {Some{value} == Model.observe(T, d, _, route(d, i)) : Maybe<&2, T>}
239  %extent : {Some{value} == Model.observe(T, d, array, route_n(d, _, i)) : Maybe<&2, T>}
240  observed