coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: rcp AT Cs.Nott.AC.UK
- To: Edsko de Vries <devriese AT cs.tcd.ie>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] More dependent pattern matching
- Date: 09 Jun 2008 16:13:46 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
- Source-info: From (or Sender) name not authenticated.
I'm stuck again in trying to write some dependent code. I want to index avec A n is isomorphic to (Fin n -> A). If you intend to work with both vec and Fin, you should define this isomorphism, and you'd then be able to get the function you want rather easily.
vector:
Section vectors.
Variable (A : Set).
Inductive vec : nat -> Set :=
| vnil : vec 0
| vcons : forall n, A -> vec n -> vec (S n).
Inductive fin : nat -> Set :=
| finz : fin 1
| fins : forall n, fin n -> fin (S n). Fixpoint vind n (i : fin n) {struct i} : vec n -> A :=
match i in fin n return vec n -> A with
| finz => fun v => match v in vec m return (match m with 0 => True | S _ => A end) with
| vnil => I
| vcons _ x _ => x
end
| fins m j => fun v =>
match v in vec m return (match m with 0 => True | S _ => A end) with
| vnil => I
| vcons m' _ xs => vind m j xs (* wrong *)
end
end.
Best,
RP>
This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.
- [Coq-Club] More dependent pattern matching, Edsko de Vries
- Re: [Coq-Club] More dependent pattern matching,
Adam Chlipala
- Re: [Coq-Club] More dependent pattern matching, Edsko de Vries
- Re: [Coq-Club] More dependent pattern matching,
Conor McBride
- Re: [Coq-Club] More dependent pattern matching, Conor McBride
- Re: [Coq-Club] More dependent pattern matching,
Edsko de Vries
- Re: [Coq-Club] More dependent pattern matching, Conor McBride
- <Possible follow-ups>
- Re: [Coq-Club] More dependent pattern matching, rcp
- Re: [Coq-Club] More dependent pattern matching,
Adam Chlipala
Archive powered by MhonArc 2.6.16.