- tuple-head tup nprocedure
function (result)
(tuple-head tup n) requires (and (%tuple? tup) (<= n (%tuple-length tup))) ensures (and (%tuple result) (= (%tuple-length result) n))
function (result)
(tuple-head tup n) requires (and (%tuple? tup) (<= n (%tuple-length tup))) ensures (and (%tuple result) (= (%tuple-length result) n))