The Coq mailing list

["J. Zhang" <j.l.zhang AT durham.ac.uk>]

Dear all,

 

I am considering to give definition of dependent vector on Coq. It seems in Coq library there is no such datatype, isn't it? Can I get some hint how to think to startup the work.

 

Cheers

 

Jack

 

________________________

 

Jack Zhang PhD student
University of Durham, UK
Science Lab, South Road
Durham, DH1 3LE
________________________