def high

bendtorch-core@0.1.0.0 · src/storage/array.bend:34

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

34def high(-T: Data, -d: Nat, -original: Array<T>, -path: Model.Path(d), xs: Array<T>,
35  read: Read<T, d, original, path>, -ex: Model.Balanced(T, d, xs)) ->
36  Read<T, 1n+d, ANode{xs, original}, Model.Step{True{}, path}>:
37  match read:
38    case Read{ys, value, ey, kept, observed}:
39      Read{ANode{xs, ys}, value, (ex, ey),
40        Equal.cong(Array<T>, Array<T>, y => ANode{xs, y}, ys, original, kept), observed}