- vector->tuple vecprocedure
function (result)
(vector->tuple vec) requires (vector? vec) ensures (and (%tuple? result) (= (%tuple-length result) (vector-length vec)))
function (result)
(vector->tuple vec) requires (vector? vec) ensures (and (%tuple? result) (= (%tuple-length result) (vector-length vec)))