~/jendhub

def get_retained

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

import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
import Base

276def get_retained(-T: Data, -d: Nat, -original: Array<T>, -i: U32,
277  cert: GetFull<T, d, original, i>) -> {first(T, Array.get(T, original, i)) == original : Array<T>}:
278  match cert:
279    case GetFull{array, value, equal, kept, observed, valid}:
280      %equal : {first(T, _) == original : Array<T>}
281      kept

Uses (6)

Used by (1)