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