def low

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

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

26def low(-T: Data, -d: Nat, -original: Array<T>, -path: Model.Path(d), ys: Array<T>,
27  read: Read<T, d, original, path>, -ey: Model.Balanced(T, d, ys)) ->
28  Read<T, 1n+d, ANode{original, ys}, Model.Step{False{}, path}>:
29  match read:
30    case Read{xs, value, ex, kept, observed}:
31      Read{ANode{xs, ys}, value, (ex, ey),
32        Equal.cong(Array<T>, Array<T>, x => ANode{x, ys}, xs, original, kept), observed}