coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] (no subject)

From: Jean-Christophe Filliatre <Jean-Christophe.Filliatre AT lri.fr>
To: "J. Zhang" <j.l.zhang AT durham.ac.uk>
Cc: <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club] (no subject)
Date: Fri, 31 Jan 2003 17:38:26 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

> 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.

As  far  as  the Coq  library  is  concerned,  nothing has  been  done
regarding dependent vectors.

But  you'll  find  many  variations  on dependent  lists  in  the  Coq
contributions  (http://coq.inria.fr/contribs-eng.html).   One  is  for
instance "hardware" (http://coq.inria.fr/contribs/hardware.html),
which contains dependent lists in

        CIRCUITS/Libraries/Lib_Lists/Dependent_lists.v

Hope this helps,
--
Jean-Christophe

[Coq-Club] (no subject), satrajit
- Re: [Coq-Club] (no subject), Jean Goubault-Larrecq
- Re: [Coq-Club] (no subject), Jean-Christophe Filliatre
- <Possible follow-ups>
- [Coq-Club] (no subject), J. Zhang
  - Re: [Coq-Club] (no subject), Jean-Christophe Filliatre