def retained_correct

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

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/array.bend as ArrayCore

62def retained_correct(-T: Data, -d: Nat, -array: Array<T>, -path: Model.Path(d),
63  read: ArrayCore.Read<T, d, array, path>) ->
64  {ArrayCore.retained(T, d, array, path, read) == array : Array<T>}:
65  match read:
66    case ArrayCore.Read{retained, value, balanced, kept, observed}:
67      kept