Hi.
I'm clueless at the moment how the _implicit existential_ for
-----------------------------------------------------------------------
( xs : Vec m X ; ys : Vec n X !
let !------------------------------!
! vrevacc' xs ys :[ âlâVec l X])
vrevacc' xs ys <= rec xs
{ vrevacc' xs ys <= case xs
{ vrevacc' vnil ys [=> ys]
vrevacc' (vcons x xs) ys => vrevacc' xs (vcons x ys)
}
}
------------------------------------------------------------------------
on page 9 should work or will work. I don't know how to make the
connection from n to l or how plain old ys of type Vec n X can serve as
an appropriate outcome.
The only way I can complete the program which returns (also) a vector of
_some_ length is to use dependent pairing, like Thorsten shows it in the
accompaniment to his course.
-------------------------------------------------------------------------
( A : * ; B : A -> * ! ( a : A ; b : B a !
data !---------------------! where !----------------------!
! Sigma A B : * ) ! pair a b : Sigma A B )
-------------------------------------------------------------------------
( xs : Vec m X ; ys : Vec n X !
let !-----------------------------------------------!
! vrevacc' xs ys : Sigma Nat (lam l => Vec l X) )
vrevacc' xs ys <= rec xs
{ vrevacc' xs ys <= case xs
{ vrevacc' vnil ys => pair n ys
vrevacc' (vcons x xs) ys => vrevacc' xs (vcons x ys)
}
}
-------------------------------------------------------------------------
Best regards,
Sebastian
