def clone_first
bendtorch-core@0.1.0.0 · src/storage/certificates.bend:19
import bendtorch-core@0.1.0.0/src/storage/certificates.bend as Certificates
import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/clone.bend as Clone
19def clone_first(-T: Data, +d: Nat, original: Array<T>, -result: Array<T> & Array<T>,
20 equal: {result == Array.clone(T, original) : Array<T> & Array<T>},
21 valid: Model.Balanced(T, d, original)) -> Model.Balanced(T, d, Pair.fst(Array<T>, Array<T>, result)):
22 %Equal.sym(Array<T> & Array<T>, result, Array.clone(T, original), equal) :
23 Model.Balanced(T, d, Pair.fst(Array<T>, Array<T>, _))
24 Clone.first_balanced(T, d, original, Clone.certify(T, d, original, valid))