def certify

bendtorch-core@0.1.0.0 · src/storage/size.bend:29

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

29def certify(-T: Data, +d: Nat, array: Array<T>, valid: Model.Balanced(T, d, array)) -> Sized<T, d, array>:
30  match d array:
31    case 0n ALeaf{x}:
32      Sized{ALeaf{x}, 1, {==}, {==}, {==}, valid}
33    case 0n ANode{xs, ys}:
34      match valid:
35    case 1n+p ALeaf{x}:
36      match valid:
37    case 1n++p ANode{xs, ys}:
38      (ex, ey) = valid
39      join(T, p, xs, ys, certify(T, p, xs, ex), ey)