The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hi,

  Let me make my point again: what you see is not what you get ([Print f])! 
The definition of f that goes into the kernel does not contain the let 
binding anymore, so SN is preserved, and all reduction strategies work. 
Extraction will use the kernel term as well, not the pre-term wrote by 
the user. 

Cheers,
— Matthieu

On 12 févr. 2014, at 00:57, Greg Morrisett 
<greg AT eecs.harvard.edu>
 wrote:

> 
> On Feb 11, 2014, at 6:54 PM, Mitchell Wand 
> <wand AT ccs.neu.edu>
>  wrote:
> 
>> Is this a CBN vs. CBV issue?
> 
> Yes.  I'd argue that if termination checking is allowing for:
> 
>  Fixpoint f (x:nat) : nat := let z := f(x) in 0
> 
> then the language isn't confluent, and so it's easy to run into
> problems when reduction is done one way, and extraction + evaluation
> is done another.
> 
> But I suspect Pierre was smart enough to cover the bases here
> and it's not really a problem.  I was just hoping someone knew
> what, exactly, is going on.
> 
> -Greg