def clone_second
bendtorch-core@0.1.0.0 · src/storage/certificates.bend:26
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
26def clone_second(-T: Data, +d: Nat, original: Array<T>, -result: Array<T> & Array<T>,
27 equal: {result == Array.clone(T, original) : Array<T> & Array<T>},
28 valid: Model.Balanced(T, d, original)) -> Model.Balanced(T, d, Pair.snd(Array<T>, Array<T>, result)):
29 %Equal.sym(Array<T> & Array<T>, result, Array.clone(T, original), equal) :
30 Model.Balanced(T, d, Pair.snd(Array<T>, Array<T>, _))
31 Clone.second_balanced(T, d, original, Clone.certify(T, d, original, valid))