The Coq mailing list

["Klaus Weich" <Klaus.Weich AT web.de>]

Pierre Letouzey 
<letouzey AT lri.fr>
 schrieb am 27.07.01:
> 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
> 
> 
>  

Note that the ocaml-compiler (at least the native one) produces, for

(match f n1 n3 with Left -> Left | Right -> Right)

or

(f n1 n3)

the same code. I.e. this optimization is already done by the (native code) 
ocaml-compiler.
_______________________________________________________________________
1.000.000 DM gewinnen - kostenlos tippen - http://millionenklick.web.de
IhrName AT web.de,
 8MB Speicher, Verschluesselung - http://freemail.web.de