coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: beginner's question

From: Pierre Letouzey <letouzey AT lri.fr>
To: Michel Levy <Michel.Levy AT imag.fr>
Cc: <coq-club AT pauillac.inria.fr>
Subject: Re: beginner's question
Date: Thu, 26 Jul 2001 10:55:28 +0200 (CEST)

On Thu, 26 Jul 2001, Michel Levy wrote:

>
> Why (match f n1 n3 with Left -> Left | Right -> Right) is no replaced by
> (f n1 n3) ?
>

Because of lazyness of the programmer in charge of the extraction part,
who is ... me.
There are some trivial optimization of this kind that should be added
like the constant one (match ... with Left -> Left | Right -> Left to be
replaced by Left).

It will be done, I promise. I just don't know when...

--
Pierre Letouzey
---------------
letouzey AT lri.fr
Tel:01 69 15 42 35 (France)
http://www.lri/~letouzey

beginner's question, Michel Levy
- Re: beginner's question, Pierre Letouzey