def get_observed
bendtorch-core@0.1.0.0 · src/storage/refinement.bend:283
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
283def get_observed(-T: Data, -d: Nat, -original: Array<T>, -i: U32,
284 cert: GetFull<T, d, original, i>) ->
285 {Some{second(T, Array.get(T, original, i))} ==
286 Model.observe(T, d, original, route(d, i)) : Maybe<&2, T>}:
287 match cert:
288 case GetFull{array, value, equal, kept, observed, valid}:
289 %equal : {Some{second(T, _)} == Model.observe(T, d, original, route(d, i)) : Maybe<&2, T>}
290 observed