coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: beginner's questions

From: Jean-Christophe Filliatre <Jean-Christophe.Filliatre AT lri.fr>
To: David Monniaux <monniaux AT clipper.ens.fr>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: beginner's questions
Date: Tue, 6 Jan 1998 09:14:46 +0100

> * CRYPTIC ERROR MESSAGE
> Also, why is the following code incorrect?
> Fixpoint extract [l: list] : {i: nat | (lt i (length l))} -> nat :=
>   [ii: {i: nat | (lt i (length l))}]
> ...
> Error message : Illegal application (Non-functional construction) :
> ...

You're  right: it is  a   bug in the    V6.1, which have  been  fixed.
Everything works  fine in  our development version  of  Coq (6.2, soon
available).

--
Jean-Christophe FILLIATRE

mailto:Jean-Christophe.Filliatre AT lri.fr
  http://www.lri.fr/~filliatr

beginner's questions, David Monniaux
- Re: beginner's questions, Jean-Christophe Filliatre
- Re: beginner's questions, Jean-fr MONIN - FT.BD/CNET/DTL/MSV