def observed_correct

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

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

55def observed_correct(-T: Data, -d: Nat, -array: Array<T>, -path: Model.Path(d),
56  read: ArrayCore.Read<T, d, array, path>) ->
57  {ArrayCore.observation(T, d, array, path, read) == Model.observe(T, d, array, path) : Maybe<&2, T>}:
58  match read:
59    case ArrayCore.Read{retained, value, balanced, kept, observed}:
60      observed