coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: David Pichardie <david.pichardie AT irisa.fr>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] cases analysis on Coq
- Date: Wed, 05 Mar 2003 14:13:38 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
I'm not a coq expert but I can propose you a quick answer.
In order to define this
with a fixpoint definition, you have to use annotation cases :Variable c :nat.
Definition f := (Vec_rec [n:nat;l:(Vec n)](Vec n)
nil
[n:nat][a:nat][l:(Vec n)][l':(Vec n)](cons n (mult a c) l')).
Fixpoint f_fix [c,n:nat;v:(Vec n)] : (Vec n) :=
<[n:nat;v:(Vec n)](Vec n)>Cases v of
nil => nil
| (cons k a l) => (cons k (mult a c) (f_fix c k l))
end.
Eval Compute in (f_fix (2) O nil).
Eval Compute in (f_fix (2) (2) (cons (1) (10) (cons (0) (100) nil))).
because the result depends on k (section 1.2.9 of Coq manual).
Hope this helps,
David.
- [Coq-Club] cases analysis on Coq, J. Zhang
- Re: [Coq-Club] cases analysis on Coq, Jean-Francois Monin
- Re: [Coq-Club] cases analysis on Coq, David Pichardie
Archive powered by MhonArc 2.6.16.