coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] finite sets and vectors

From: Venanzio Capretta <Venanzio.Capretta AT mathstat.uottawa.ca>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] finite sets and vectors
Date: Fri, 24 Jun 2005 10:32:25 -0400
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi,

Inductive Fin: nat -> Set :=
fin: forall i m:nat, Fin (S (i+m)).

Isn't this the best definition of finite types?

Inductive Vec (A:Set): nat -> Set :=
vec: forall l:list A, Vec A (length l).

And isn't this the best definition of vectors?

--
Venanzio Capretta
Department of Mathematics
and Statistics
University of Ottawa, Canada
http://www.science.uottawa.ca/~vcapr396/

[Coq-Club] finite sets and vectors, Venanzio Capretta