def written_transport

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

import Base
import bendtorch-core@0.1.0.0/src/storage/array.bend as Core
import bendtorch-core@0.1.0.0/src/storage/size.bend as Size

312def written_transport(-T: Data, -d: Nat, -array: Array<T>, -original: Array<T>,
313  -n: U32, -i: U32, -new: T, -result: Array<T>,
314  kept: {array == original : Array<T>}, extent: {n == Size.capacity(d) : U32},
315  written: {result == Core.write_path(T, d, array, route_n(d, n, i), new) : Array<T>}) ->
316  {result == Core.write_path(T, d, original, route(d, i), new) : Array<T>}:
317  %kept : {result == Core.write_path(T, d, _, route(d, i), new) : Array<T>}
318  %extent : {result == Core.write_path(T, d, array, route_n(d, _, i), new) : Array<T>}
319  written