- 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)))