chickadee
»
tuples
»
tuple->vector
Identifier search
tuple->vector
tup
procedure
function (result)
(
tuple->vector tup
)
requires
(
%tuple? tup
)
ensures
(
vector? result
)