Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] cases analysis on Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] cases analysis on Coq


chronological Thread 
  • 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
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')).
 
with a fixpoint definition, you have to use annotation cases :

 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.



Archive powered by MhonArc 2.6.16.

Top of Page