- ral-join head tailprocedure
-
function (result) requires (and (ral? head) (ral? tail) (eq? (ral-item? head) (ral-item? tail))) ensures (and (ral? result) (fx= (ral-count result) (fx+ (ral-count head) (ral-count tail))))
function (result) requires (and (ral? head) (ral? tail) (eq? (ral-item? head) (ral-item? tail))) ensures (and (ral? result) (fx= (ral-count result) (fx+ (ral-count head) (ral-count tail))))