coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] cbv evaluation in Coq?
Date: Wed, 13 Jan 2016 15:49:45 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mailinglists AT robbertkrebbers.nl; spf=None smtp.mailfrom=mailinglists AT robbertkrebbers.nl; spf=None smtp.helo=postmaster AT smtp1.science.ru.nl
Ironport-phdr: 9a23:30j8YxTr7n0Fj7WsYYfyRXgE5tpsv+yvbD5Q0YIujvd0So/mwa64YRWN2/xhgRfzUJnB7Loc0qyN4/6mCTNLv83JmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvipduDPE4W33KUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGfayQ6NtRrtBST8iLmod5cvxtBCFQxHcyGEbVzAslRBCDhLZpDLgU537vzHh/r540SiePMv5SbEvRS+K9aBhQhLylCQdOjQz/XvMzMp02vEI6Cm9rgByltaHKLqeM+BzK/vQ

On 01/13/2016 03:44 PM, Matthieu Sozeau wrote:

You are right that the cbv strategy is doing normalization under
binders though, not weak reduction as advertised.

Thanks for clarifying. But is this a bug or intended behavior?

[Coq-Club] cbv evaluation in Coq?, Randy Pollack, 01/13/2016
- Re: [Coq-Club] cbv evaluation in Coq?, Robbert Krebbers, 01/13/2016
  - Re: [Coq-Club] cbv evaluation in Coq?, Gabriel Scherer, 01/13/2016
    - Re: [Coq-Club] cbv evaluation in Coq?, Matthieu Sozeau, 01/13/2016
      - Re: [Coq-Club] cbv evaluation in Coq?, Robbert Krebbers, 01/13/2016
        
        Re: [Coq-Club] cbv evaluation in Coq?, Randy Pollack, 01/13/2016
        
        Re: [Coq-Club] cbv evaluation in Coq?, Hugo Herbelin, 01/14/2016