def grow_balanced

bendtorch-core@0.1.0.0 · src/storage/api.bend:323

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
import bendtorch-core@0.1.0.0/src/storage/clone.bend as Clone

323def grow_balanced(+d: Nat, array: Array<F32>, +effect: Effect, valid: Model.Balanced(F32, d, array)) ->
324  Model.Balanced(F32, d, grow(array, effect)):
325  match effect:
326    case Wrote{+i, +w}:
327      Refinement.law_set_balanced(F32, d, array, i, w, valid)
328    case Kept{+i}:
329      Refinement.law_get_balanced(F32, d, array, i, valid)
330    case Left{}:
331      Clone.first_balanced(F32, d, array, Clone.certify(F32, d, array, valid))
332    case Right{}:
333      Clone.second_balanced(F32, d, array, Clone.certify(F32, d, array, valid))